Naso (Jul 19 2023 at 10:56): Naso (Jul 19 2023 at 10:56):image.png
Is this a bug? I essentially have
the two lines here are identical yet there is a type error. I.e. i essentially have
moreover have "... = x"
moreover have "... = x" (* type unification failed *)
the second line with the error I assume should desugar to moreover have "x = x" and should not be a type error!?
Mathias Fleury (Jul 19 2023 at 14:13):in the "| a b C c" remove the "c", which is not used anywhere
Mathias Fleury (Jul 19 2023 at 14:14):currently it is here and must have a type
Mathias Fleury (Jul 19 2023 at 14:14):due to that, there is the "'a itself" you are seeing
Mathias Fleury (Jul 19 2023 at 14:14):and it does not type
Mathias Fleury (Jul 19 2023 at 14:15):Alternative: give c a type in each expression and the 'a itself will disappear
Last updated: Apr 27 2024 at 16:16 UTC