Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- This file: -- http://anggtwu.net/LEAN/checksyntax.lean.html -- http://anggtwu.net/LEAN/checksyntax.lean -- (find-angg "LEAN/checksyntax.lean") -- Author: Eduardo Ochs <[email protected]> -- Based on code by Kyle Miller. -- -- See: (find-es "lean" "checksyntax") -- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20do.20I.20write.20a.20.22.23check_syntax.22.3F/near/438919441 -- -- (defun e () (interactive) (find-angg "LEAN/checksyntax.lean")) import Lean.Elab.Command namespace Playground2 scoped syntax "⊥" : term scoped syntax "⊤" : term scoped syntax:40 term " OR " term : term scoped syntax:50 term " AND " term : term elab "#check_syntax " t:term : command => do Lean.logInfo m!"{t}" elab "#check_syntax " t:term : command => do Lean.logInfo m!"{repr t.raw}" #check_syntax 42 + "foo" #check_syntax ⊥ OR (⊤ AND ⊥) end Playground2 -- Local Variables: -- coding: utf-8-unix -- End: