Consider the following div function written in Coq. It takes in a proof that the divider is non-zero.
Definition div (n d:nat) (pf: ~(d = 0)) := n/d.
~(d = 0): Is this a term or a type? My understanding is that this is a term of type
Check gives the same.
Check (forall d:nat, ~(d = 0)) forall d : nat, d <> 0 : Prop
pf a member of the term
~(d = 0)? This is confusing. Should I now think of
~(d = 0) as a type? Note that I am familiar with dependent types (though not expert) and am being pedantic here.
A term by itself cannot be a type unless
pf : ~(d = 0) is a syntactic sugar for something along the lines of
pf: Proof ~(d = 0) where
Proof is a type of kind $\Pi x:Prop. \star$. That is, it takes a prop term and returns a new type.
What is going on here? I think I am missing the calculus part here.