mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
19 lines
284 B
Idris
19 lines
284 B
Idris
|
module Postfix
|
||
|
|
|
||
|
|
record Diag (a : Type) where
|
||
|
|
fstt : a
|
||
|
|
sndd : a
|
||
|
|
equal : fstt === sndd
|
||
|
|
|
||
|
|
val : Diag a -> a
|
||
|
|
val diag = diag .fstt
|
||
|
|
|
||
|
|
prf : (d : Diag a) -> val d === d.sndd
|
||
|
|
prf = ?a
|
||
|
|
|
||
|
|
(.val') : Diag a -> a
|
||
|
|
diag .val' = diag .sndd
|
||
|
|
|
||
|
|
sym : (d : Diag a) -> d .fstt === d .val'
|
||
|
|
sym = ?b
|