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

simplify some matches

Browse source
This commit is contained in:
rhiannon morris 2023-01-09 23:45:21 +01:00
parent 82795e9976
commit f405aeb7f9
2 changed files with 8 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
lib/Quox/Syntax/Qty/Three.idr
View file

@ -45,13 +45,11 @@ data Compat3 : Rel Three where
public export
compat3 : Dec2 Compat3
compat3 pi rh with (decEq pi rh)
compat3 pi pi | Yes Refl = Yes CmpRefl
compat3 pi rh | No ne with (decEq rh Any)
compat3 pi Any | No ne | Yes Refl = Yes CmpAny
compat3 pi rh | No ne | No na = No $ \case
CmpRefl => ne Refl
CmpAny => na Refl
compat3 pi rh with (decEq pi rh) | (decEq rh Any)
compat3 pi pi | Yes Refl | _ = Yes CmpRefl
compat3 pi Any | No _ | Yes Refl = Yes CmpAny
compat3 pi rh | No ne | No na =
No $ \case CmpRefl => ne Refl; CmpAny => na Refl
public export

7
lib/Quox/Syntax/Var.idr
View file

@ -240,10 +240,9 @@ eqReflect : (i, j : Var n) -> (i = j) `Reflects` (i == j)
eqReflect VZ VZ = RTrue Refl
eqReflect VZ (VS i) = RFalse absurd
eqReflect (VS i) VZ = RFalse absurd
eqReflect (VS i) (VS j) with (eqReflect i j)
eqReflect (VS i) (VS j) | r with (i == j)
eqReflect (VS i) (VS j) | RTrue yes | True = RTrue $ cong VS yes
eqReflect (VS i) (VS j) | RFalse no | False = RFalse $ no . injective
eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
_ | RTrue yes | True = RTrue $ cong VS yes
_ | RFalse no | False = RFalse $ no . injective
public export
reflectToDec : p `Reflects` b -> Dec p