From 3850059ee28e82a5259f797ccd243c0d13ba73d4 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 6 Feb 2024 13:07:20 +0100 Subject: [PATCH] Fix import in README.Data.Fin.Substitution.UntypedLambda Also import this module in doc/README.agda so that it is covered by CI. Closes #2278. --- doc/README.agda | 4 ++++ doc/README/Data/Fin/Substitution/UntypedLambda.agda | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/README.agda b/doc/README.agda index 41b536a0d0..6a9a3e398c 100644 --- 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 index 126959958f..036f7ed5ca 100644 --- 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; ε; _◅_)