From bb10205c22e4518f286ab59ad0e23b14756ec851 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 20 Oct 2025 22:26:30 +0200 Subject: some simplifications --- Nominal/Basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'Nominal') diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean index 2858516..7bc6e1c 100644 --- a/Nominal/Basic.lean +++ b/Nominal/Basic.lean @@ -22,20 +22,20 @@ class PermSet (X : Type) extends MulAction (FPerm 𝔸) X /-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where smul π a := π a - one_smul := by aesop - mul_smul := by aesop + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl /-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 (FPerm 𝔸) where smul π τ := π * τ - one_smul := by aesop - mul_smul := by aesop + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl /-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/ def PermSet.discrete (X : Type) : PermSet 𝔸 X where smul π x := x - one_smul := by aesop - mul_smul := by aesop + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl /-- We consider Unit a discrete (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit -- cgit v1.3.1