FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Resugar: improve resugaring for projectors #3341

Closed mtzguido closed 2 days ago

mtzguido commented 2 days ago

It was not properly handling cases where the field is a function, that can be further applied. Noticed this while debugging a proof.

Before: Screenshot 2024-07-03 140333 After: Screenshot 2024-07-03 140136

And with implicits: Before: Screenshot 2024-07-03 140042 After: Screenshot 2024-07-03 140126

mtzguido commented 2 days ago

Linking #3227, #3283, #3294