Idris2/libs/contrib/Syntax/WithProof.idr

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)
Add libraries 2020-05-18 15:59:07 +03:00			`module Syntax.WithProof`

Let DocComments trough from Lexer to Parser 2020-05-25 13:21:09 +03:00			`prefix 10 @@`

Add libraries 2020-05-18 15:59:07 +03:00			`\|\|\| 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)`