[isabelle] Type Coercions?


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?

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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