mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
0655d3d96d
decl syntax [lhs] = decl1 decl2 ... The lhs has the same form as expression syntax rules, except that any names bounds in braces {n} are replaced in top level name bindings as well as explicit lambda/pi/let bindings. This is mostly intended to be used in conjection with top level %runElab declarations, but probably has wider use. |
||
---|---|---|
.. | ||
expected | ||
run | ||
syntax002.idr |