Re: [isabelle] Dependent types
I think that this particular definition means nothing more than the following:
mkMyNum :: "[nat list, nat list] => bool"
M: "mkMyNum xs (n#xs)"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and