0 | module Syntax.WithProof 1 | 2 | export prefix 10 @@ 3 | 4 | ||| Until Idris2 supports the 'with (...) proof p' construct, here's a 5 | ||| poor-man's replacement. 6 | public export 7 | (@@) : (t : a) -> (u : a ** t = u) 8 | (@@) x = (x ** Refl) 9 |