From 281326b9b7eb6561526f02ff37eab9c39aa83b58 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 22 Oct 2025 23:34:14 +0200
Subject: always require infinite, countable, equality-decidable atoms

---
 Nominal/Instances.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Nominal/Instances.lean')

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index 057a0de..dcf079f 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -8,7 +8,7 @@ import Nominal.Support
 This file contains common instances of (FPerm 𝔸)-sets and nominal sets.
 -/
 
-variable (𝔸 : Type)
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 /-!
 ## Atoms
@@ -25,7 +25,7 @@ instance : NominalSet 𝔸 𝔸 where
     intro a; use {a}
     exact ⟨NominalSet.supp_atom' 𝔸, Set.finite_singleton a⟩
 
-lemma NominalSet.supp_atom [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
+lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
   ext b; constructor
   · apply support_subset_supp 𝔸
     · exact NominalSet.supp_atom' 𝔸
@@ -90,7 +90,7 @@ section Products
 
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where
 
-variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by
   intro π hπ
@@ -135,7 +135,7 @@ section Coproducts
 
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where
 
-variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by
   intro π hπ
-- 
cgit v1.3.1