mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
22 lines
527 B
Idris
22 lines
527 B
Idris
|
infixl 0 ~~
|
||
|
|
prefix 1 |~
|
||
|
|
infix 1 ...
|
||
|
|
|
||
|
|
public export
|
||
|
|
(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
|
||
|
|
(...) x pf = (x ** pf)
|
||
|
|
|
||
|
|
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 z
|
||
|
|
|
||
|
|
public export
|
||
|
|
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x = y
|
||
|
|
Calc (|~ x) = Refl
|
||
|
|
Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der
|
||
|
|
|
||
|
|
bad : Z = S Z
|
||
|
|
bad = Calc $ |~ Z ~~ Z ...(Refl)
|