diff --git a/Bigop.lean b/Bigop.lean index eb575a9..5adf4ec 100644 --- a/Bigop.lean +++ b/Bigop.lean @@ -116,7 +116,7 @@ syntax "def_bigop" str term:max term:max : command -- `F` is inserted only in the second expansion, the expansion of the new macro `$head`. macro_rules | `(def_bigop $head $op $unit) => - `(macro $head:strLit "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F)) + `(macro $head:str "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F)) def_bigop "SUM" Nat.add 0 #check SUM (i <- [0, 1, 2]) i+1 diff --git a/Expander.lean b/Expander.lean index 8d71e3d..4732a3b 100644 --- a/Expander.lean +++ b/Expander.lean @@ -124,8 +124,8 @@ partial def expand : Syntax → ExpanderM Syntax | `(fun $id:ident => $e) => do let e ← withLocal (getIdentVal id) (expand e) `(fun $id:ident => $e) - | `($num:numLit) => `($num:numLit) - | `($str:strLit) => `($str:strLit) + | `($num:num) => `($num:num) + | `($str:str) => `($str:str) | `($n:quotedName) => `($n:quotedName) | `($fn $args*) => do let fn ← expand fn @@ -195,8 +195,8 @@ partial def pp : Syntax → Format | ps => ppIdent id.getId ++ bracket "{" (joinSep (ps.map (format ∘ Prod.fst)) ", ") "}" | `(fun ($id : $ty) => $e) => paren f!"fun {paren (pp id ++ " : " ++ pp ty)} => {pp e}" | `(fun $id => $e) => paren f!"fun {pp id} => {pp e}" - | `($num:numLit) => format (num.isNatLit?.getD 0) - | `($str:strLit) => repr (str.isStrLit?.getD "") + | `($num:num) => format (num.isNatLit?.getD 0) + | `($str:str) => repr (str.isStrLit?.getD "") | `($fn $args*) => paren <| pp fn ++ " " ++ joinSep (args.toList.map pp) line | `(def $id:ident := $e) => f!"def {ppIdent id.getId} := {pp e}" | `(syntax $[(name := $n)]? $[(priority := $prio)]? $[$args:stx]* : $kind) => "syntax ..." -- irrelevant for this example diff --git a/lean-toolchain b/lean-toolchain index a992958..3a406d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-05 +leanprover/lean4:nightly-2022-04-02