diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index f2bf90d..460c7ae 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -186,7 +186,7 @@ class NominalSet (X : Type) extends PermSet 𝔸 X where fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite /-- A discrete nominal set where permutations do not change anything. -/ -class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X where +class NominalSet.Discrete (X : Type) extends NominalSet 𝔸 X where is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x namespace NominalSet |