Re: [isabelle] Type Coercions?



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

Tobias

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.