From 281326b9b7eb6561526f02ff37eab9c39aa83b58 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 22 Oct 2025 23:34:14 +0200 Subject: always require infinite, countable, equality-decidable atoms --- Nominal/Permutations.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Nominal/Permutations.lean') 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 -- cgit v1.3.1