From 68832dc6f28cbc10d9861d8202382689984e06ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2014 12:07:13 -0800 Subject: [PATCH] fix(builtin/macros): comments Signed-off-by: Leonardo de Moura --- src/builtin/macros.lua | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/builtin/macros.lua b/src/builtin/macros.lua index db0ae3aec..8566ab70b 100644 --- a/src/builtin/macros.lua +++ b/src/builtin/macros.lua @@ -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 = {}