All Questions
Tagged with soft-question programming-languages
2
questions
4
votes
1
answer
252
views
How can you represent a dependent type visually?
So, obviously for a term $t$ of type $T$, I would represent it as:
T
+-----------+
| |
| t |
| |
+-----------+
That is a node ...
1
vote
1
answer
561
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 ...