From e02ad2dcc0f93107c18f8316b386b92b45548e97 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 30 Nov 2025 22:20:35 +0100 Subject: update lean --- Nominal/LambdaCalculus/Preterms.lean | 2 +- Nominal/LambdaCalculus/Terms.lean | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) (limited to 'Nominal/LambdaCalculus') diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean index 74f7397..c133343 100644 --- a/Nominal/LambdaCalculus/Preterms.lean +++ b/Nominal/LambdaCalculus/Preterms.lean @@ -114,7 +114,7 @@ instance : NominalSet Var Preterm where simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq] simp only [PermSet.fix, vars, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ exact ⟨hπ.left, a_ih.left hπ.right⟩ - · simp [vars, Set.Finite.insert, a_ih] + · simp [vars, a_ih] · constructor · intro π hπ simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq] diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index 2118156..c698b65 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -229,7 +229,12 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (by intro t u htu cases htu - sorry) + · sorry + · sorry + · sorry + · sorry + · sorry + · sorry) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x -- cgit v1.3.1