Does anybody know of any good resources regarding
Ξ΄-reduction (delta-reduction), ie. reducing primitive functions in lambda calculus?
barrywatson.se/lsi/lsi_delta_
Saw it in Section 3 of leodemoura.github.io/files/elaborat, but couldn't find any further references to it in that section. π€
Conversation
Replying to
These seem to talk about slightly different things; there is no such reduction of "primitives" in Lean. The environment is a map from constants (names) to definitions, and delta-reduction is substitution along that map, no further computation involved.
1
2
(Also note that many parts of the paper like unification constraints are outdated regarding Lean 3 and beyond)
1
Show replies