idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 19:13:02 +03:00
Code Issues Projects Releases Wiki Activity

Try a fix for the preorder reasoning error

Browse Source 
Correct the dependency in `FastDerivation` to use the RHS in `step`
Try to avoid shadowing `y` in the LHS of `Calc`
This commit is contained in:
Ohad Kammar 2020-08-09 06:57:29 +01:00 committed by Ohad Kammar
parent d387c76e9b
commit ff76dee6c7
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -19,12 +19,12 @@ public export
public export public export
data FastDerivation : (x : a) -> (y : b) -> Type where data FastDerivation : (x : a) -> (y : b) -> Type where
(|~) : (x : a) -> FastDerivation x x (|~) : (x : a) -> FastDerivation x x
(~~) : FastDerivation x y -> (step : (z : c ** y ~=~ z)) -> FastDerivation x z (~~) : FastDerivation x y -> (step : (z : c ** y ~=~ z)) -> FastDerivation x (fst step)
public export public export
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y
Calc (|~ x) = Refl Calc (|~ x) = Refl
Calc {y} ((~~) {z=y} {y=y} der (y ** Refl)) = Calc der Calc {y} ((~~) {z=_} {y=_} der (_ ** Refl)) = Calc der
{- -- requires import Data.Nat {- -- requires import Data.Nat
0 0