The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

tumenjargal tsagaan wrote:
> Hi All,
>
> I wanted to rewrite coq-code in a sequence form.
> Is there any automated tool for this purpose?
>
> even better is it if possible in a tex format.
>
> Thank you a lot.
>
> Best regards,
>
> Tumee.
>
>
>
>
>
>       
>   
> Sorry, I mean how to represent coq-code in the form of inference rules.
> e.g.
> Inductive Nat : Set := zero : Nat
>                       | succ : Nat -> Nat.
> We can put this code in the form of two inference rules like this:
>
>                           \forall n : Nat
> -------- zero       -----------------  succ
> zero: Nat           succ n : Nat
>
>
> Are there any automated tools?
>
> Thanks.
>
>   
I don't know of any tool to do this.

Yves