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

make Definitions.isZero a predicate

Browse source
This commit is contained in:
rhiannon morris 2023-01-21 01:41:21 +01:00
parent 1dc0c913e7
commit 8a2eea22fb
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
lib/Quox/Definition.idr
View file

@ -12,7 +12,7 @@ record AnyTerm q where
get : forall d, n. Term q d n get : forall d, n. Term q d n
public export public export
record Definition' q (isGlobal : q -> Type) where record Definition' q (isGlobal : Pred q) where
constructor MkDef' constructor MkDef'
qty : q qty : q
type : AnyTerm q type : AnyTerm q
@ -46,12 +46,18 @@ public export %inline
(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal (.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
g.qtyP = Element g.qty g.qtyGlobal g.qtyP = Element g.qty g.qtyGlobal
public export %inline
isZero : IsQty q => Definition q -> Bool
isZero g = isYes $ isZero g.qty
public export public export
0 Definitions' : (q : Type) -> (q -> Type) -> Type 0 IsZero : IsQty q => Pred $ Definition q
IsZero g = IsZero g.qty
public export %inline
isZero : (p : IsQty q) => Dec1 $ Definition.IsZero @{p}
isZero g = isZero g.qty
public export
0 Definitions' : (q : Type) -> Pred q -> Type
Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
public export public export