change data to record definition

martinescardo · Sep 19, 2024 · c62468a · c62468a
1 parent 24712f6
commit c62468a
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 11 deletions.
diff --git a/source/DiscreteGraphicMonoids/Free.lagda b/source/DiscreteGraphicMonoids/Free.lagda
@@ -73,7 +73,7 @@ module free-discrete-graphic-monoid-development
        where
 
  M-is-discrete : is-discrete M
- M-is-discrete = discrete'-gives-discrete M-is-discrete'
+ M-is-discrete = discrete'-gives-discrete
 
  f' : List X → M
  f' []       = e

diff --git a/source/DiscreteGraphicMonoids/LWRDGM.lagda b/source/DiscreteGraphicMonoids/LWRDGM.lagda
@@ -31,7 +31,7 @@ module _
 
  private
   d : is-discrete X
-  d = discrete'-gives-discrete d'
+  d = discrete'-gives-discrete
 
  graphical⁻ : graphical (_·_ {𝓤} {X})
  graphical⁻ (xs , a) (ys , b) =

diff --git a/source/DiscreteGraphicMonoids/ListsWithoutRepetitions.lagda b/source/DiscreteGraphicMonoids/ListsWithoutRepetitions.lagda
@@ -33,7 +33,7 @@ module _
 
  private
   d : is-discrete X
-  d = discrete'-gives-discrete d'
+  d = discrete'-gives-discrete
 
 \end{code}
 
@@ -394,7 +394,7 @@ module _ {X : 𝓤 ̇ }
 
  private
   d : is-discrete X
-  d = discrete'-gives-discrete d'
+  d = discrete'-gives-discrete
 
  η⁻ : X → List⁻ X
  η⁻ x = (x • []) , refl
@@ -607,7 +607,7 @@ module _ {X : 𝓤 ̇ }
  δ-map : (z : X) (xs : List X)
        → δ (f z) (map f (δ z xs)) ＝ δ (f z) (map f xs)
  δ-map z [] = refl
- δ-map z (x • xs) = h (discrete'-gives-discrete X-is-discrete' z x)
+ δ-map z (x • xs) = h (discrete'-gives-discrete z x)
   where
    h : is-decidable (z ＝ x)
      → δ (f z) (map f (δ z (x • xs))) ＝ δ (f z) (map f (x • xs))
@@ -629,7 +629,7 @@ module _ {X : 𝓤 ̇ }
     δ (f z) (map f (x • xs))       ∎
      where
       I = ap (λ - → δ (f z) (map f -)) (δ-≠ z x xs u)
-      II = g (discrete'-gives-discrete Y-is-discrete' (f z) (f x))
+      II = g (discrete'-gives-discrete (f z) (f x))
        where
         g : is-decidable (f z ＝ f x)
           → δ (f z) (f x • map f (δ z xs)) ＝ δ (f z) (f x • map f xs)

diff --git a/source/DiscreteGraphicMonoids/ListsWithoutRepetitionsMore.lagda b/source/DiscreteGraphicMonoids/ListsWithoutRepetitionsMore.lagda
@@ -32,7 +32,7 @@ module _
 
  private
   d : is-discrete X
-  d = discrete'-gives-discrete d'
+  d = discrete'-gives-discrete
 
  _∉_ _∈_ : X → List X → 𝓤 ̇
  x ∉ xs = ρ (x • xs) ＝ x • ρ xs

diff --git a/source/UF/DiscreteAndSeparated.lagda b/source/UF/DiscreteAndSeparated.lagda
@@ -760,11 +760,13 @@ Added 1st May 2024. Wrapper for use with instance arguments:
 
 \begin{code}
 
-data is-discrete' {𝓤 : Universe} (X : 𝓤 ̇ ) : 𝓤 ̇ where
- discrete-gives-discrete' : is-discrete X → is-discrete' X
+record is-discrete' {𝓤 : Universe} (X : 𝓤 ̇ ) : 𝓤 ̇ where
+ constructor
+  discrete-gives-discrete'
+ field
+  discrete'-gives-discrete : is-discrete X
 
-discrete'-gives-discrete : {X : 𝓤 ̇ } → is-discrete' X → is-discrete X
-discrete'-gives-discrete (discrete-gives-discrete' d) = d
+open is-discrete' {{...}} public
 
 \end{code}