Skip to content

Commit

Permalink
Fix import in README.Data.Fin.Substitution.UntypedLambda
Browse files Browse the repository at this point in the history 
Closes #2278.
  • Loading branch information
@andreasabel
andreasabel committed Feb 6, 2024
1 parent e2bd4c5 commit d7afe98
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/README/Data/Fin/Substitution/UntypedLambda.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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; ε; _◅_)
Expand Down

1 comment on commit d7afe98

@jamesmckinna
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved! (but others eg @MatthewDaggitt may wish to fix up the GitHub history/labelling/milestones before committing...?)

Please sign in to comment.