From a4a279e6a3162354398083f24d93fa6388f37652 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Tue, 10 Sep 2024 13:52:11 +0200 Subject: [PATCH] Compatibility with Agda 2.7/Stdlib 2.1.1 --- Class/MonadTC.agda | 4 ++-- README.md | 2 ++ Tactic/Extra.agda | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Class/MonadTC.agda b/Class/MonadTC.agda index 35b2622..25bc490 100644 --- a/Class/MonadTC.agda +++ b/Class/MonadTC.agda @@ -106,13 +106,13 @@ record MonadTC (M : ∀ {f} → Set f → Set f) -- TODO: return true on function, axiom and prim-fun constructors? isDef : Name → M Bool isDef n = do - constructor′ _ ← getDefinition n + constructor′ _ _ ← getDefinition n where _ → return true return false isCon : Name → M Bool isCon n = do - constructor′ _ ← getDefinition n + constructor′ _ _ ← getDefinition n where _ → return false return true diff --git a/README.md b/README.md index 7a5aab7..863c2c3 100644 --- a/README.md +++ b/README.md @@ -11,5 +11,7 @@ We mirror the version numbers of [agda-stdlib](https://github.com/agda/agda-stdl | [v2.6.3](https://github.com/agda/agda/releases/tag/v2.6.3) | [v1.7.2](https://github.com/agda/agda-stdlib/releases/tag/v1.7.2) | [v1.7.2](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v1.7.2) | [v1.7.2](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v1.7.2) | | [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v1.7.3](https://github.com/agda/agda-stdlib/releases/tag/v1.7.3) | [v1.7.3](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v1.7.3) | [v1.7.3](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v1.7.3) | | [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v2.0](https://github.com/agda/agda-stdlib/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.0) | +| [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v2.0](https://github.com/agda/agda-stdlib/releases/tag/v2.1) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.1) | +| [v2.7.0](https://github.com/agda/agda/releases/tag/v2.7.0) | [v2.1.1](https://github.com/agda/agda-stdlib/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.1.1](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.1.1) | Minor revisions will append to these major versions (e.g. `v1.7.3b` or `v1.7.3.10`). diff --git a/Tactic/Extra.agda b/Tactic/Extra.agda index 0be4568..39334cd 100644 --- a/Tactic/Extra.agda +++ b/Tactic/Extra.agda @@ -169,7 +169,7 @@ getPatTele cn = do print $ "Getting pattern telescope for constructor: " ◇ show cn ty ← getType cn print $ " ty: " ◇ show ty - data-cons n ← getDefinition cn + data-cons n _ ← getDefinition cn where _ → _IMPOSSIBLE_ print $ " n: " ◇ show n data-type ps _ ← getDefinition n