[isabelle] Dependent types



Hi all,

I have some coq proofs that I am considering converting to Isabelle.
However, the coq proofs use dependent types, similar to this:

    Inductive MyNum (from : list nat) (to : list nat) : Type
        := mkMyNum : forall (myNum : nat)
                            (valid : to = cons myNum from),
                     MyNum from to.

Can anyone tell me what the best way to handle this in Isabelle would be
please?


Thanks
Ian






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.