infix は notation に展開されるマクロ

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

15 stars 5 forks source link

infix は notation に展開されるマクロ #402

Open Seasawher opened 3 days ago

Seasawher commented 3 days ago

elab "#expand_command " t:command : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => 
    logInfo m!"{t}"

/-- info: notation:50 lhs✝:51 " LXOR " rhs✝:50 => (fun l r => (!l && r)) lhs✝ rhs✝ -/
#guard_msgs in #expand_command infixr:50 " LXOR " => fun l r => (!l && r)