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

Author: plt-amy

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:

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