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

preorder reasoning: introduce a Step datatype (#734)

Browse Source 
Refactor the DIY equational reasoning library to be a bit more like
the generic pre-order reasoning library:

Change the `...` notation into a constructor for a new `Step` datatype.

This seems to help idris disambiguate between the two kinds of
reasoning when they're used in the same file (e.g., frex).

Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
This commit is contained in:
Ohad Kammar 2020-10-07 17:44:18 +01:00 committed by GitHub
parent 0c1a124704
commit ef730c7eb1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -13,18 +13,18 @@ infix 1 ...
|||```
|||and we can think of the `...( justification )` as ASCII art for a thought bubble.
public export
(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
(...) x pf = (x ** pf)
data Step : a -> b -> Type where
(...) : (0 y : a) -> (0 step : x ~=~ y) -> Step x y
public export
data FastDerivation : (x : a) -> (y : b) -> Type where
(|~) : (x : a) -> FastDerivation x x
(~~) : FastDerivation x y -> (step : (z : c ** y ~=~ z)) -> FastDerivation x (fst step)
(|~) : (0 x : a) -> FastDerivation x x
(~~) : FastDerivation x y -> {0 z : a} -> (step : Step y z) -> FastDerivation x z
public export
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x ~=~ y
Calc (|~ x) = Refl
Calc ((~~) {y=_} der (_ ** Refl)) = Calc der
Calc ((~~) {y=_} der (_ ... Refl)) = Calc der
{- -- requires import Data.Nat
0