search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Handle casts in lra parser #82

Closed proux01 closed 1 year ago

pi8027 commented 1 year ago

A type cast t : T is represented as a let-in let x : T := t in x in Coq-Elpi. I guess the ring and field tactics have the same issue.

This would be a good occasion to think about supporting let-ins in general, using the PHOAS representation presented in Reification by Parametricity, although it would be a bit tricky in combination with homomorphism applications, e.g., considering let x := t in f x + g x where both f and g are homomorphisms.

proux01 commented 1 year ago

I guess the ring and field tactics have the same issue.

I don't know how it's handled there but all my tests with ring did work. The issue doesn't seem to be there.

This would be a good occasion to think about supporting let-ins in general, using the PHOAS representation presented in Reification by Parametricity, although it would be a bit tricky in combination with homomorphism applications.

Sure, but given how annoying is the bug I'd first merge this as a quick fix.