HomeIsabelle/Phabricator
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.

Written by makarius on Sep 22 2021, 12:17 PM.
User
Projects
None
Subscribers
None

Event Timeline