Re: [isabelle] Dependent types

I don't speak Coq very well, but if this defines some subset of nat
lists, the conversion may work according to the following general
schema: replace the dependent type by some unconstrained type (eg nat
list), introduce predicates that check that some nat list satisfies the
constraints in the dependent type, and make those predicates
preconditions in your theorems whenever needed. You recast the type
constraints as explicit formulas.


Ian Lynagh wrote:
> 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.