mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
10 lines
208 B
Idris
10 lines
208 B
Idris
module Syntax.WithProof
|
|
|
|
prefix 10 @@
|
|
|
|
||| Until Idris2 supports the 'with (...) proof p' construct, here's a
|
|
||| poor-man's replacement.
|
|
public export
|
|
(@@) : (t : a) -> (u : a ** t = u)
|
|
(@@) x = (x ** Refl)
|