Skip to content

Update blockOnMeta → blockTC #1972

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MatthewDaggitt merged 7 commits into from
Oct 13, 2023
Merged

Update blockOnMeta → blockTC #1972

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
eed4c34
Update blockOnMeta → blockTC
plt-amy May 30, 2023
32b5937
Update ci-ubuntu.yml to latest version of Agda
MatthewDaggitt Aug 20, 2023
a0a74ec
Undo bump of experimental
MatthewDaggitt Oct 13, 2023
5cb8f3d
Merge branch 'master' into aliao/agda-6033
MatthewDaggitt Oct 13, 2023
9a598e9
Ensure backwards compatability
MatthewDaggitt Oct 13, 2023
0e3458c
Ensure backwardwards compatibility
MatthewDaggitt Oct 13, 2023
fbf4761
Undo unnecessary change
MatthewDaggitt Oct 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
7 changes: 5 additions & 2 deletions src/Reflection/TCM.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

------------------------------------------------------------------------
Expand All @@ -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
Expand Down