Conversation
…d two more counterexamples for eta-functions ; spelling fixes
…case in Converter.agda
…'m not sure if it is sound
jespercockx
left a comment
jespercockx
left a comment
There was a problem hiding this comment.
Good job! I have some small-ish formatting and style remarks but otherwise this looks good.
… TVar is on right
| conversionProof <- convertCheck newScope b term | ||
| return (CEtaFunctions x functionTerm b conversionProof) | ||
| convertWhnf r a b = do | ||
| conversionProof <- convertCheck r b a |
There was a problem hiding this comment.
Won't calling convertCheck here go into an infinite loop in case the two sides are not convertible? (Or at least, loop until the fuel is exhausted.) I don't think it's possible to have a generic catch-all case for symmetry like this in the conversion checker, we have to manually apply symmetry in the cases where it's needed.
test/EtaFunctionsExplDefArg.agda
Outdated
| eta-higher = λ A B C → λ f → refl | ||
|
|
||
| eta-counterexample-simple : addOne ≡ (λ x → (suc (const Nat x x))) | ||
| eta-counterexample-simple = refl No newline at end of file |
There was a problem hiding this comment.
Again Github indicates there's a missing newline here.
|
@diode-lang could you please not merge PRs when there are still open comments on it? In this case they were minor but in general it's better to wait. Also, I prefer rebases over merges. (I guess I should change the settings of this repo for both these things.) |
2 participants
This pull request adds eta-equality for functions to Agda Core and is partial work for #34.
It adds:
ToCore.hswhich meant that any.agdaprograms withTDataorTDefwould previously crash. I'm still looking for a fix such that parameter lists and indices are correctly translated forTDataConversion.agdaandConverter.agdaEtaFunctionsChurch.agda