rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

use stdlib Elem and add note why not also stdlib OpenUnion

Browse source
This commit is contained in:
rhiannon morris 2021-09-26 10:55:07 +02:00
parent 2b1a043280
commit 65e45dcc79
1 changed files with 4 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Quox/Error.idr
View file

@ -1,5 +1,7 @@
module Quox.Error module Quox.Error
import Data.List.Elem
import Control.Monad.Identity import Control.Monad.Identity
import Control.Monad.Trans import Control.Monad.Trans
import Control.Monad.Reader import Control.Monad.Reader
@ -10,20 +12,6 @@ import Control.Monad.RWS
%default total %default total
||| a proof that an element is in a list. unlike the standard library one, this
||| is represented as a single number at runtime.
public export
data Elem : a -> List a -> Type where
Here : x `Elem` (x :: xs)
There : x `Elem` xs -> x `Elem` (y :: xs)
%builtin Natural Elem
export
Uninhabited (x `Elem` []) where
uninhabited Here impossible
uninhabited (There _) impossible
||| a representation of a list's length. this is used in the `Ord` instance to ||| a representation of a list's length. this is used in the `Ord` instance to
||| transform the `Ord` constraints into `Eq`s ||| transform the `Ord` constraints into `Eq`s
public export public export
@ -40,6 +28,8 @@ record OneOf types where
constructor One constructor One
elem : type `Elem` types elem : type `Elem` types
1 value : type 1 value : type
-- this is basically the same as Data.OpenUnion, but using Elem instead of
-- AtIndex is much easier for some stuff here e.g. `get`
export export
Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem