Rename FiniteNonEmpty to FiniteInhabited

parent 1d533191
\begin{code}
module Data.FiniteInhabited where
open import Data.FiniteInhabited.Base public
\end{code}
\begin{code}
module Data.FiniteInhabited.Base where
open import Data.Finite.Base using (Finite; module Finite)
\end{code}
%<*FiniteInhabited>
\AgdaTarget{FiniteInhabited}
\begin{code}
record FiniteInhabited {ℓ} (α : Set ℓ) : Set ℓ where
field finite : Finite α
default : α
open Finite finite public
\end{code}
%</FiniteInhabited>
\begin{code}
module Data.FiniteInhabited.Bool where
open import Data.Bool.Base using (Bool; false)
open import Data.FiniteInhabited.Base using (FiniteInhabited)
open import Data.Finite.Bool using (Finite-Bool)
\end{code}
\begin{code}
instance
\end{code}
%<*FiniteInhabited-Bool>
\AgdaTarget{FiniteInhabited-Bool}
\begin{code}
FiniteInhabited-Bool : FiniteInhabited Bool
FiniteInhabited-Bool = record { finite = Finite-Bool
; default = false }
\end{code}
%</FiniteInhabited-Bool>
\begin{code}
module Data.FiniteNonEmpty where
open import Data.FiniteNonEmpty.Base public
\end{code}
......@@ -5,7 +5,7 @@ open import Data.Fin using (Fin)
open import Relation.Binary using (DecSetoid; Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; decSetoid)
open import Data.FiniteNonEmpty.Base using (FiniteNonEmpty)
open import Data.FiniteInhabited.Base using (FiniteInhabited)
\end{code}
......@@ -15,10 +15,10 @@ open import Data.FiniteNonEmpty.Base using (FiniteNonEmpty)
record Atomic : Set₁ where
constructor MkAtomic
field Atom : Set
enum : FiniteNonEmpty Atom
enum : FiniteInhabited Atom
_≟A_ : Decidable {A = Atom} _≡_
open FiniteNonEmpty enum public
open FiniteInhabited enum public
|Atom| = #α
Atom# = Fin #α
......@@ -32,8 +32,8 @@ record Atomic : Set₁ where
%<*Atomic-default-decEq>
\AgdaTarget{MkAtomic′}
\begin{code}
MkAtomic′ : (Atom : Set) (enum : FiniteNonEmpty Atom) → Atomic
MkAtomic′ Atom enum = let open FiniteNonEmpty enum using (_≟ⁿ_) in MkAtomic Atom enum _≟ⁿ_
MkAtomic′ : (Atom : Set) (enum : FiniteInhabited Atom) → Atomic
MkAtomic′ Atom enum = let open FiniteInhabited enum using (_≟ⁿ_) in MkAtomic Atom enum _≟ⁿ_
\end{code}
%</Atomic-default-decEq>
......
......@@ -3,7 +3,7 @@ module PiWare.Atomic.Bool where
open import Data.Bool.Base using (Bool) renaming (_≟_ to _≟Bool_)
open import Data.FiniteNonEmpty.Bool using (FiniteNonEmpty-Bool)
open import Data.FiniteInhabited.Bool using (FiniteInhabited-Bool)
open import PiWare.Atomic using (Atomic)
\end{code}
......@@ -13,7 +13,7 @@ open import PiWare.Atomic using (Atomic)
\begin{code}
Atomic-Bool : Atomic
Atomic-Bool = record { Atom = Bool
; enum = FiniteNonEmpty-Bool
; enum = FiniteInhabited-Bool
; _≟A_ = _≟Bool_ }
\end{code}
%</Atomic-Bool>
......@@ -15,9 +15,9 @@ import Data.Finite.Bool
import Data.Finite.Forall
import Data.Finite
import Data.FiniteNonEmpty.Base
import Data.FiniteNonEmpty.Bool
import Data.FiniteNonEmpty
import Data.FiniteInhabited.Base
import Data.FiniteInhabited.Bool
import Data.FiniteInhabited
import Data.HVec
import Data.IVec
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment