diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index dd9b9d2..c8fdd86 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -136,10 +136,10 @@ Sets equipped with a permutation operation. -/ section PermSet -variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] - /-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/ -class PermSet (X : Type) extends MulAction (FPerm 𝔸) X +class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) extends MulAction (FPerm 𝔸) X + +variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] /-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where |