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

slight simplify

Browse source
This commit is contained in:
rhiannon morris 2023-02-14 21:16:20 +01:00
parent c40e6a60ff
commit 802dfae493
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Syntax/DimEq.idr
View file

@ -75,13 +75,13 @@ C eqs :<? d = C $ eqs :< d
private %inline private %inline
ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d) ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
ifVar i p = map $ \q => if isYes $ q `decEq` B i then p else q ifVar i p = map $ \q => if q == B i then p else q
-- (using decEq instead of (==) because of the proofs below)
private %inline private %inline
checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
checkConst Zero Zero eqs = C eqs checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
checkConst One One eqs = C eqs
checkConst _ _ _ = ZeroIsOne
export export
setConst : Var d -> DimConst -> DimEq' d -> DimEq d setConst : Var d -> DimConst -> DimEq' d -> DimEq d