Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: ML antiquotation "instantiate"

view this post on Zulip Email Gateway (Oct 28 2021 at 20:05):

From: Makarius <>
* ML *

Examples in HOL:

fun make_assoc_type (A, B) =
\<^instantiate>‹'a = A and 'b = B in typ ‹('a × 'b) list››;

val make_assoc_list =
map (fn (x, y) =>
\<^instantiate>‹'a = ‹fastype_of x› and 'b = ‹fastype_of y› and
x and y in term ‹(x, y)› for x :: 'a and y :: 'b›);

fun symmetry x y =
\<^instantiate>‹'a = ‹Thm.ctyp_of_cterm x› and x and y in
lemma ‹x = y ⟹ y = x› for x y :: 'a by simp›

fun symmetry_schematic A =
\<^instantiate>‹'a = A in
lemma (schematic) ‹x = y ⟹ y = x› for x y :: 'a by simp›

This refers to Isabelle/54085e37ce4d. Some applications are in the preceeding

Proper documentation will follow shortly after Isabelle2021-1-RC1 (start of
next week).


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC