diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bfd659aa9..d012d754a2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3801,6 +3801,15 @@ This is a full list of proofs that have changed form to use irrelevant instance WellFounded _<_ → Irreflexive _≈_ _<_ ``` +* Added new types and operations to `Reflection.TCM`: + ``` + Blocker : Set + blockerMeta : Meta → Blocker + blockerAny : List Blocker → Blocker + blockerAll : List Blocker → Blocker + blockTC : Blocker → TC A + ``` + * Added new file `Relation.Binary.Reasoning.Base.Apartness` This is how to use it: diff --git a/src/Reflection/TCM.agda b/src/Reflection/TCM.agda index a3df1f1bc3..d762dab2c5 100644 --- a/src/Reflection/TCM.agda +++ b/src/Reflection/TCM.agda @@ -8,8 +8,9 @@ module Reflection.TCM where -open import Reflection.AST.Term import Agda.Builtin.Reflection as Builtin + +open import Reflection.AST.Term import Reflection.TCM.Format as Format ------------------------------------------------------------------------ @@ -29,7 +30,9 @@ open Builtin public ; getContext; extendContext; inContext; freshName ; declareDef; declarePostulate; defineFun; getType; getDefinition ; blockOnMeta; commitTC; isMacro; withNormalisation - ; debugPrint; noConstraints; runSpeculative) + ; debugPrint; noConstraints; runSpeculative + ; Blocker; blockerMeta; blockerAny; blockerAll; blockTC + ) renaming (returnTC to pure) open Format public