Commit 9e407525 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files


parent ae02d3c0
......@@ -19,7 +19,7 @@ Inductive ord :=
Note that this inductive type does satisfy the strict positivity constraint: constructor `lim` has an argument of type `nat->ord`, where `ord` appears indeed on the right. Having instead `lim:(ord->nat)->ord` would be refused by Coq.
We can plunge in this type the usual natural numbers of type `nat`.
For instance via a mixte addition `add : ord -> nat -> ord` :
For instance via a mixed addition `add : ord -> nat -> ord` :
Fixpoint add a n :=
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment