From 52da7e6960ea5eedb7374be07aa065a8f34128b8 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 24 Oct 2025 00:15:26 +0200 Subject: refactor namespaces --- Nominal/Support.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Nominal/Support.lean') 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 -- cgit v1.3.1