API for open (as in free variables) terms#714

Closed

gares wants to merge 22 commits intoLPCIC:masterfrom ybertot:extensional-replace

+436-1

Commits on Nov 7, 2024

Commits on Nov 11, 2024

fixes identify proofs in applications (needed a sigma), plus csmetics
ybertot
committed

Commits on Nov 12, 2024

failed attempt at coping with polymorphic functions
ybertot
committed

Commits on Nov 13, 2024

this version handles polymorphic functions gracefully, the examples are well
ybertot
committed
illustrate problems with variable renaming, adds an example where bound
ybertot
committed
adds the case where sections are used, which currently makes elpi replace fail
ybertot
committed