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