idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Change PreorderReasoning arguments to 0

Browse Source
This commit is contained in:
Giuseppe Lomurno 2021-02-12 16:36:38 +01:00 committed by André Videla
parent bd21fd51e2
commit 440e60a00b
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/contrib/Syntax/PreorderReasoning.idr
View File

@ -22,7 +22,7 @@ data FastDerivation : (x : a) -> (y : b) -> Type where
(~~) : FastDerivation x y -> (step : Step y z) -> FastDerivation x z
public export
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y
Calc : {0 x : a} -> {0 y : b} -> FastDerivation x y -> x ~=~ y
Calc (|~ x) = Refl
Calc ((~~) der (_ ...(Refl))) = Calc der

4
libs/contrib/Syntax/PreorderReasoning/Generic.idr
View File

@ -18,12 +18,12 @@ data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
-> FastDerivation leq x z
public export
CalcWith : Preorder dom leq => {x,y : dom} -> FastDerivation leq x y -> x `leq` y
CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> FastDerivation leq x y -> x `leq` y
CalcWith (|~ x) = reflexive x
CalcWith ((<~) der (z ... step)) = transitive {po = leq} _ _ _ (CalcWith der) step
public export
(~~) : {x,y : dom}
(~~) : {0 x : dom} -> {0 y : dom}
-> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
-> FastDerivation leq x z
(~~) der (z ... Refl) = der