ML antiquotations for type constructors and term constants
ML
- ML antiquotations for type constructors and term constants:
- Type‹c›
- Type‹c T …› ― ‹same with type arguments›
- Type_fn‹c T …› ― ‹fn abstraction, failure via exception TYPE›
- Const‹c›
- Const‹c T …› ― ‹same with type arguments›
- Const‹c for t …› ― ‹same with term arguments›
- Const_‹c …› ― ‹same for patterns: case, let, fn›
- Const_fn‹c T …› ― ‹fn abstraction, failure via exception TERM›
Examples in HOL:
val natT = \<^Type>‹nat›; fun mk_funT (A, B) = \<^Type>‹fun A B›; val dest_funT = fn \<^Type>‹fun A B› => (A, B); fun mk_conj (A, B) = \<^Const>‹conj for A B›; val dest_conj = fn \<^Const_>‹conj for A B› => (A, B); fun mk_eq T (t, u) = \<^Const>‹HOL.eq T for t u›; val dest_eq = fn \<^Const_>‹HOL.eq T for t u› => (T, (t, u));
This refers to Isabelle/4974c3697fee.
- Projects
- None
- Subscribers
- None