Questions tagged [abstract-syntax-tree]

Use this tag with abstract syntax trees.

Filter by
Sorted by
Tagged with
1 vote
2 answers
183 views

How to parse Lean 3(?) theorem statements to JSON AST

I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
Michael Norrish's user avatar
0 votes
1 answer
20 views

Induction error on mutually defined types in Coq

I want to define two types that depend on each other ...
matteo_c's user avatar
  • 131
0 votes
1 answer
104 views

How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages". On PDF page 28 you'll see an OCaml ...
Daniel Donnelly's user avatar
1 vote
1 answer
342 views

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

Question: Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms. I'm wondering whether Lean4 (or a typical well-known PA) just ...
Daniel Donnelly's user avatar
6 votes
0 answers
170 views

How does one systematically traverse OCaml representations of Coq ASTs terms?

I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language). My main challenge is to figure out how to do this systematically because I ...
Charlie Parker's user avatar
8 votes
1 answer
173 views

How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...
Molly Stewart-Gallus's user avatar