michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(builtin/macros): comments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-06 12:07:13 -08:00
parent 929a536e2f
commit 68832dc6f2
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/builtin/macros.lua
View file

@ -11,15 +11,15 @@
--
-- Example: suppose we invoke
--
-- binder_macro("for", Const("ForallIntro"), 3, 1, 3)
-- binder_macro("take", Const({"forall", "intro"}), 3, 1, 3)
--
-- Then, the macro expression
--
-- for x y : Int, H x y
-- take x y : Int, H x y
--
-- produces the expression
--
-- ForallIntro Int _ (fun x : Int, ForallIntro Int _ (fun y : Int, H x y))
-- forall::intro Int _ (fun x : Int, forall::intro Int _ (fun y : Int, H x y))
--
-- The _ are placeholders (aka) holes that will be filled by the Lean
-- elaborator.
@ -49,18 +49,18 @@ function binder_macro(name, f, farity, typepos, lambdapos)
precedence)
end
-- The following macro is used to create nary versions of operators such as MP and ForallElim.
-- The following macro is used to create nary versions of operators such as mp.
-- Example: suppose we invoke
--
-- nary_macro("mp", Const("MP"), 4)
-- nary_macro("mp'", Const("mp"), 4)
--
-- Then, the macro expression
--
-- mp Foo H1 H2 H3
-- mp' Foo H1 H2 H3
--
-- produces the expression
--
-- (MP (MP (MP Foo H1) H2) H3)
-- (mp (mp (mp Foo H1) H2) H3)
function nary_macro(name, f, farity)
local bin_app = function(e1, e2)
local args = {}