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

Uninhabited instances

Browse source
This commit is contained in:
rhiannon morris 2022-08-22 10:07:46 +02:00
parent 77e94a3033
commit 6dd18d89bd
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Syntax/Qty.idr
View file

@ -74,7 +74,11 @@ data IsSubj : Qty -> Type where
SZero : IsSubj Zero SZero : IsSubj Zero
SOne : IsSubj One SOne : IsSubj One
export Uninhabited (IsSubj Any) where uninhabited _ impossible
public export public export
data IsGlobal : Qty -> Type where data IsGlobal : Qty -> Type where
GZero : IsGlobal Zero GZero : IsGlobal Zero
GAny : IsGlobal Any GAny : IsGlobal Any
export Uninhabited (IsGlobal One) where uninhabited _ impossible