Re: [isabelle] Dependent types



I think that this particular definition means nothing more than the following:

inductive
  mkMyNum :: "[nat list, nat list] => bool"
where
  M: "mkMyNum xs (n#xs)"

Larry Paulson


On 6 Apr 2010, at 22:20, 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.