git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/libs/base/Syntax/PreorderReasoning.idr
17 lines 574 B history raw
1module Syntax.PreorderReasoning
3%access public export
5-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.
6syntax [expr] "QED" = qed expr
7-- foo ={ prf }= bar ={ prf' }= fnord QED
8-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
9syntax [from] "={" [prf] "}=" [to] = step from prf to
11namespace Equal
12 using (a : Type, x : a, y : a, z : a)
13 qed : (x : a) -> x = x
14 qed x = the (x = x) Refl
15 step : (x : a) -> x = y -> (y = z) -> x = z
16 step x Refl Refl = Refl