Remove tilde files added by accident

parent 4272e9dd
\begin{code}
module Data.FiniteNonEmpty.Base where
open import Data.Finite.Base using (Finite; module Finite)
\end{code}
%<*FiniteNonEmpty>
\AgdaTarget{FiniteNonEmpty}
\begin{code}
record FiniteNonEmpty {ℓ} (α : Set ℓ) : Set ℓ where
field finite : Finite α
default : α
open Finite finite public
\end{code}
%</FiniteNonEmpty>
\begin{code}
module Data.FiniteNonEmpty.Bool where
open import Data.Bool.Base using (Bool; false)
open import Data.FiniteNonEmpty.Base using (FiniteNonEmpty)
open import Data.Finite.Bool using (Finite-Bool)
\end{code}
\begin{code}
instance
\end{code}
%<*FiniteNonEmpty-Bool>
\AgdaTarget{FiniteNonEmpty-Bool}
\begin{code}
FiniteNonEmpty-Bool : FiniteNonEmpty Bool
FiniteNonEmpty-Bool = record { finite = Finite-Bool
; default = false }
\end{code}
%</FiniteNonEmpty-Bool>
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