Hi,
Is it possible to define the following datatype in HOL4?
exp =
Var of num
| App of exp # exp
| Abs of (num -> exp)
When the above is given to HOL_datatype, it responds:
Can't find definition for nested type: fun
(This datatype comes from Adam Chlipala's Coq paper at POPL'10.)
Thanks,
Magnus
------------------------------------------------------------------------------
The Planet: dedicated and managed hosting, cloud storage, colocation
Stay online with enterprise data centers and the best network in the business
Choose flexible plans and management services without long-term contracts
Personal 24x7 support from experience hosting pros just a phone call away.
http://p.sf.net/sfu/theplanet-com
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
