Re: [isabelle] Type Coercions?

Yes, it would be nice to have coercions inserted automatically. But no
such luck in Isabelle.


Christian Doczkal wrote:
> Hello
> I just played around a little with the Coq proof assistant and noted the
> feature of Coercions
> You can spare yourself some typing and improve readability of the input
> code by telling the system how to resolve some "typing error" with some
> explicit coercion function.
> For example when working with locally nameless terms one can use
>> Coercion bvar : nat >-> exp.
> The Coq interpreter then inserts the constructor bvar whenever it
> expects an exp but finds a nat instead. So one can write (abs 0) instead
> of (abs (bvar 0)). (with abs :: exp => exp)
> Can a similar effect be achieved in Isabelle/HOL as well?

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