Stream: Coq devs & plugin devs

Topic: "Anomaly "conversion was given unreduced term (FLambda)." wi


view this post on Zulip Robbert Krebbers (Oct 03 2023 at 13:15):

I ran into this issue when updating one of the Iris projects to Coq 8.18, see https://gitlab.mpi-sws.org/iris/actris/-/jobs/252795 It happens with a setoid_rewrite where rewriting happens below a binder (i.e., in a case where normal rewrite fails).

Anyone experience with debugging these FLambda error messages? I have not seen them before, and my attempts to minimize the problem have failed so far.

view this post on Zulip Notification Bot (Oct 03 2023 at 13:25):

This topic was moved here from #Coq users > "Anomaly "conversion was given unreduced term (FLambda)." wi by Karl Palmskog.

view this post on Zulip Karl Palmskog (Oct 03 2023 at 13:25):

since anomalies are (nearly by definition) problems in Coq itself, I move this topic here to get more dev eyes on it

view this post on Zulip Pierre-Marie Pédrot (Oct 04 2023 at 06:36):

This kind of problem is typically due to the legacy unification sending ill-typed terms to conversion. The FLambda thing happens when there is an eta-expansion needed somewhere but one side has a non-functional type.


Last updated: Oct 13 2024 at 01:02 UTC