Eta conversion for functions#60

Merged

diode-lang merged 34 commits intomainfrom

Feb 3, 2026

Commits on Dec 5, 2025

Experimenting with what agda-core allows and does not allow
diode-lang
committed

Commits on Dec 12, 2025

This "fix" seems to do something desirable(?)
diode-lang
committed

Commits on Dec 17, 2025

Commits on Dec 19, 2025

Possible definition which would require eta-conversion in the type checker
diode-lang
committed

Commits on Jan 5, 2026

Fix likely bug in pretty printer
diode-lang
committed

Commits on Jan 6, 2026

Marks place in code where eta-functions conversion should happen ; Add two more counterexamples for eta-functions ; spelling fixes
diode-lang
committed

Commits on Jan 8, 2026

Commits on Jan 10, 2026

Eta conversion rule for variable and lambda (very verbose, simplify later)
diode-lang
committed

Commits on Jan 12, 2026

Some eta counterexamples get type checked
diode-lang
committed

Commits on Jan 14, 2026

Makes better eta conversion rule for vars
diode-lang
committed

Commits on Jan 15, 2026

Single rule which captures all of eta conversion for functions. But I'm not sure if it is sound
diode-lang
committed

Commits on Jan 19, 2026

Examples for eta records and eta for unit (eta for unit is non-functional)
diode-lang
committed

Commits on Jan 23, 2026

Small improvements in Conversion ; marks places where records should be added
diode-lang
committed

Commits on Jan 28, 2026

Address style improvements
diode-lang
committed

Commits on Jan 29, 2026

Commits on Feb 3, 2026