Add new blocking primitives to Reflection.TCM (agda#1972)

jamesmckinna · Nov 4, 2023 · a843d0d · a843d0d
1 parent 135951f
commit a843d0d
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 2 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -3812,6 +3812,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
@@ -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