more clever lifting of local functions about agda

[GoogleCodeExporter]

Original comment by [email protected] on 16 Jan 2008 at 12:57

• Changed state: Accepted

[GoogleCodeExporter]

The reason for the error is that the local functions are lifted to the top-level, obtaining the variables bound in the left hand side of the parent clause as arguments. In the example one of these variables (the gamma argument of /) differ in the expected type and the type of v'.

One could imagine only abstracting local functions over the variables that are actually used in the definition, but that's not something that's done at the moment.

Original comment by [email protected] on 3 Jun 2008 at 2:12

• Changed title: more clever lifting of local functions
• Added labels: Priority-Low, Type-Enhancement
• Removed labels: Priority-Medium, Type-Defect

[GoogleCodeExporter]

Original comment by [email protected] on 6 Jun 2008 at 10:24

[GoogleCodeExporter]

Fixed by adding 'Nonvariant' to polarity analysis. Now, while local function stren still takes the arguments of its superfunction as parameters, they are not used, hence analysed as 'Nonvariant' and thus ignored during equality checking.

Original comment by [email protected] on 18 Sep 2012 at 12:41

• Changed state: Fixed