The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 9 janv. 2014, at 00:31, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:

> 
> 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 ) .

Well, take the transitive closure of p <_le le_succ n m p.
— Matthieu