-- This file:
--   http://anggtwu.net/LEAN/parsediagram1.lean.html
--   http://anggtwu.net/LEAN/parsediagram1.lean
--          (find-angg "LEAN/parsediagram1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun pd () (interactive) (find-angg "LEAN/parsediagram1.lean"))
-- (defun tp () (interactive) (find-luatreeleanfile "ToPrettier1.lean"))
-- (defun o  () (interactive) (find-fline "/tmp/o"))
-- (2024tinsp 3 "fun-proj-eq")
-- (2024tinsa   "fun-proj-eq")

-- fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a
--      - -   --- -   --   - -          - -     --  -  -
--     ----- -------       ---         -----        ----
--                   ----------        -----------
--     ------------------------    ---------------------
--     

import Lean

-- fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a

#check Lean.Parser.Term.app
#check Lean.Parser.Term.basicFun
#check Lean.Parser.Term.binderIdent
#check Lean.Parser.Term.binderType
#check Lean.Parser.Term.fun
#check Lean.Parser.Term.funBinder
#check Lean.Parser.Term.hole
#check Lean.Parser.Term.ident
#check Lean.Parser.Term.implicitBinder
#check Lean.Parser.Term.instBinder
#check Lean.Parser.Term.let
#check Lean.Parser.Term.letDecl
#check Lean.Parser.Term.letPatDecl
#check Lean.Parser.Term.optIdent
#check Lean.Parser.Term.optSemicolon
#check Lean.Parser.Term.tuple
#check Lean.Parser.Term.typeAscription
#check Lean.Parser.termParser

#check `(term| 1+2)
-- #check `(typeAscription| (a b : A))

-- #check Lean.Parser.withCache

namespace Lean.Parser.Term
#check `(command|
def instBinder2 := ppGroup <| leading_parser
  "[" >> withoutPosition (optIdent >> termParser) >> "]"
)
#print instBinder

#check `(term| 1-2-3^4^5^6)

#check `(command|
@[inherit_doc] infixr:80 " ^ "   => HPow.hPow
)

-- Local Variables:
-- coding:  utf-8-unix
-- End: