diff options
| -rw-r--r-- | Nominal/Basic.lean | 12 |
1 files changed, 6 insertions, 6 deletions
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 |