diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 00:15:26 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 00:15:26 +0200 |
| commit | 52da7e6960ea5eedb7374be07aa065a8f34128b8 (patch) | |
| tree | 8f4c206936dceb94399c76b0a17852bf33cf006a /Nominal/Support.lean | |
| parent | f8b2f5190e33f3d1694442a6be32cba97fcef004 (diff) | |
refactor namespaces
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 |