From 29068d381a8b5d95c7fd4dc6111dcfb3a181f0bd Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 10 Feb 2019 03:16:51 +0100 Subject: Explicit references in antiquotations in typing.ML. Move trace switch definition to HoTT_Base. --- HoTT_Base.thy | 3 +++ typing.ML | 9 +++------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index ed8c18b..23e51e5 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -27,6 +27,9 @@ section \Setup non-core logic functionality\ declare[[eta_contract=false]] \ \Do not eta-contract\ +ML \val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\ + \ \Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\ + text \The following file sets up type assumption and inference functionality.\ ML_file "typing.ML" diff --git a/typing.ML b/typing.ML index 4bcb633..2a049d4 100644 --- a/typing.ML +++ b/typing.ML @@ -6,9 +6,6 @@ Functionality for object-level type inference. ********) -(* Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on *) -val trace = Attrib.setup_config_bool @{binding "trace"} (K false) - (* ====================================== Helper functions ====================================== *) signature TYPING_LIB = @@ -104,14 +101,14 @@ struct type jmt = term (* Determine if a term is a typing judgment *) -fun is_typing_jmt (@{const has_type} $ _ $ _) = true +fun is_typing_jmt (@{const HoTT_Base.has_type} $ _ $ _) = true | is_typing_jmt _ = false (* Functions to extract a and A from propositions "a: A" *) -fun term_of_jmt (@{const has_type} $ t $ _) = t +fun term_of_jmt (@{const HoTT_Base.has_type} $ t $ _) = t | term_of_jmt _ = Exn.error "Not a typing judgment" -fun type_of_jmt (@{const has_type} $ _ $ T) = T +fun type_of_jmt (@{const HoTT_Base.has_type} $ _ $ T) = T | type_of_jmt _ = Exn.error "Not a typing judgment" (* Get typing assumptions in "this" *) -- cgit v1.2.3