Syntax

Functions

History of functions.

Definition set of ordered pairs such that the first elements occurs at most once.

\set{(x,y)}

Multiple return values are natural, see the division algorithm. Nearly all programming language support multiple input value, some also multiple return values. Both are not strictly more expressive. Multiple return values can be implemented using tuples. Multiple inputs using currying.

Lambda calculus

Representation

Tree based syntax for proof system:

https://github.com/digama0/mm0/blob/master/mm0.md

Graphs as more fundamental

https://tiarkrompf.github.io/notes/?/graph-ir/

https://www.reddit.com/r/ProgrammingLanguages/comments/l0m5fn/graph_irs_for_expressive_languages_taming/

Coq's extensible syntax

https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#