The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Jan 8, 2014, at 5:19 PM, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:

> It would
> seem sensible to me to go the same route with inductive definitions,
> namely, rely on semantic justifications rather than syntactic ones. 

This would certainly be cool. What I do not quite understand however is what 
ordinals or well-founded relations have with such inductive definition as, 
for example, the definition of "less or equal" on nat in the Coq standard 
library?

(It's something like:

Inductive le : forall ( n m : nat ) , Type := le_refl : forall ( n : nat ) , 
le n n | le_succ : forall ( n m : nat ) , le n m -> le (S n ) ( S m ) .

)

V.