Support Agda 2.6.3 (#53)

* Support Agda 2.6.3 Everything needs to be marked `--cubical-compatible` since it all has to build together. `inc` was renamed to `inS` in Agda. Metavariables with undetermined sorts can't appear in the telescope of a clause matching on an indexed type. --------- Co-authored-by: Amélia Liao <me@amelia.how>
martinescardo · Oct 18, 2023 · 06dab2c · 06dab2c
1 parent 149882d
commit 06dab2c
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 6 deletions.
diff --git a/Agda/Cubical/cubical-prelude.lagda.md b/Agda/Cubical/cubical-prelude.lagda.md
@@ -9,8 +9,7 @@ module cubical-prelude where
 
 open import Agda.Builtin.Cubical.Path public
 open import Agda.Builtin.Cubical.Sub public
-  renaming ( inc to inS
-           ; primSubOut to outS
+  renaming ( primSubOut to outS
            )
 open import Agda.Primitive.Cubical public
   renaming ( primIMin       to _∧_  -- I → I → I
@@ -501,5 +500,3 @@ Bin→ℕ→Bin (binPos p)  = posInd localrefl (λ p _ → rem p) p
                                                               (localap sucPos (Pos→ℕ→Pos p))) ⟩
     binPos (sucPos p) ∎
 ```
-
-
diff --git a/Agda/HITs/Exercises5.lagda.md b/Agda/HITs/Exercises5.lagda.md
@@ -132,7 +132,7 @@ PathOver-endo≡ : ∀ {A : Type} {f : A → A}
                  {a a' : A} {p : a ≡ a'}
                  {q : (f a) ≡ a}
                  {r : (f a') ≡ a'}
-               → {!!}
+               → the Type {! !}
                → q ≡ r [ (\ x → f x ≡ x) ↓ p ]
 PathOver-endo≡ {p = (refl _)} {q = q} {r} h = {!!}
 

diff --git a/Agda/HITs/hits-lectures.agda-lib b/Agda/HITs/hits-lectures.agda-lib
@@ -1,2 +1,5 @@
 name: hits-lectures
 include: .
+flags:
+  --cubical-compatible
+  -WnoUnsupportedIndexedMatch
diff --git a/Agda/HITs/new-prelude.lagda.md b/Agda/HITs/new-prelude.lagda.md
@@ -144,4 +144,6 @@ data ℕ : Type where
  zero : ℕ
  suc  : ℕ → ℕ
 
+the : ∀ {l} (A : Type l) → A → A
+the _ x = x
 ```
diff --git a/Agda/Lecture-Notes/files/introduction.lagda.md b/Agda/Lecture-Notes/files/introduction.lagda.md
@@ -4,7 +4,7 @@ Notes originally written for the module *Advanced Functional Programming* of the
 
 <!--
 ```agda
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module introduction where
 ```

diff --git a/Agda/agda-lectures.agda-lib b/Agda/agda-lectures.agda-lib
@@ -4,3 +4,6 @@ include: Lecture-Notes/files
          Exercises
          Auxiliary
          Cubical
+flags:
+  -WnoUnsupportedIndexedMatch
+  --cubical-compatible
-Original file line number
+Diff line change
@@ Expand Up @@
     <!--
     ```agda
-    {-# OPTIONS --without-K --safe #-}
+    {-# OPTIONS --cubical-compatible --safe #-}
     module introduction where
     ```
@@ Expand Down @@