Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
syntaxInNamespacesAndPP.lean.out.expected
blob: 87e6dbf7f47853835f967b6cc3976d9cd535f2df [
file
] [
edit
]
true
:
Bool
true
:
Bool
meta
def
Bla
.
bla
:
Lean
.
ParserDescr
:=
Lean
.
ParserDescr
.
node
`Bla.bla 1022
(Lean.ParserDescr.binary `
andthen
(
Lean
.
ParserDescr
.
symbol
"bla"
)
(
Lean
.
ParserDescr
.
cat
`term 0))