Fix import in README.Data.Fin.Substitution.UntypedLambda (#2279)

Also import this module in doc/README.agda so that it is covered by CI. Closes #2278.
agda · Feb 7, 2024 · c8496d0 · c8496d0
1 parent 8567537
commit c8496d0
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/doc/README.agda b/doc/README.agda
@@ -222,6 +222,10 @@ import Text.Printf
 
 import README.Case
 
+-- Showcasing the framework for well-scoped substitutions
+
+import README.Data.Fin.Substitution.UntypedLambda
+
 -- Some examples showing how combinators can be used to emulate
 -- "functional reasoning"
 

diff --git a/doc/README/Data/Fin/Substitution/UntypedLambda.agda b/doc/README/Data/Fin/Substitution/UntypedLambda.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_)