search

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.
https://jonsterling.github.io/agda-calf/
Apache License 2.0
55 stars 2 forks source link

remove scary equality rules? #45

Closed jonsterling closed 1 year ago

jonsterling commented 1 year ago

These rules are true for the writer model, but extremely suspect for any other effect. index.agda builds fine with these rules replaced by the good ones (in this PR), but I noticed that many examples (under Parallel) may make use of the scary rules --- but these examples do not build even on main.