Re: [isabelle] conversion in Isabelle



> How is it possible to make conversion in Isabelle?

You apply a conversion function. The basic ones are

nat :: int => nat
int :: nat => int
real :: 'a => real

Warning: nat(i) = 0 if i<0.

> For example if i have (x::int), g^(nat x) doesnt give any error...but what type is (nat x)?

nat.

Tobias





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