-- This file:
--   http://anggtwu.net/LEAN/checksyntax.lean.html
--   http://anggtwu.net/LEAN/checksyntax.lean
--          (find-angg "LEAN/checksyntax.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- 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: