Merge remote-tracking branch 'origin/main' into broken_alive_autogene…

…rated
opencompl · May 10, 2024 · 84af681 · 84af681
2 parents f6fec7e + fab92c2
commit 84af681
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean
@@ -34,9 +34,6 @@ def empty : Ctxt Ty := []
 instance : EmptyCollection (Ctxt Ty) := ⟨Ctxt.empty⟩
 instance : Inhabited (Ctxt Ty) := ⟨Ctxt.empty⟩
 
--- TODO: write lemmas about what the empty context does.
--- We remove the @[simp] tag from empty context, to better understand
--- when we pun between context and list.
 lemma empty_eq : (∅ : Ctxt Ty) = [] := rfl
 
 @[match_pattern]
@@ -60,7 +57,7 @@ def map (f : Ty₁ → Ty₂) : Ctxt Ty₁ → Ctxt Ty₂ :=
   List.map f
 
 @[simp]
-lemma map_nil (Γ : Ctxt Ty) (t : Ty) (f : Ty → Ty') :
+lemma map_nil (f : Ty → Ty') :
   map f ∅ = ∅ := rfl
 
 @[simp]