Ohad KammarCreate a contrib directory in the standard librarybe907496 years agoHistory
8 lines · 209 B · TextRawDownload
module Syntax.WithProof ||| Until Idris2 supports the 'with (...) proof p' construct, here's a||| poor-man's replacement.prefix 10 @@public export(@@) : (t : a ) -> (u : a ** t = u)(@@) x = ( x ** Refl)

Keyboard shortcuts

General

Show keyboard shortcuts
?
Focus the current search
/

Issues and pull requests

Open filters
f

Issues, pull requests and Inbox

Select next item
j↓
Select previous item
k↑
Open selected item
Enter
Dismiss filters or clear selection
Esc

Repository code

Go to file
t