Łukasz Czajka 9f25ffde16 Detect termination for nested local definitions (#3169) ... * Closes #3147 When we call a function that is currently being defined (there may be several such due to nested local definitions), we add a reflexive edge in the call map instead of adding an edge from the most nested definition. For example, for ```juvix go {A B} (f : A -> B) : List A -> List B | nil := nil | (elem :: next) := let var1 := f elem; var2 := go f next; in var1 :: var2; ``` we add an edge from `go` to the recursive call `go f next`, instead of adding an edge from `var2` to `go f next` as before. This makes the above type-check. The following still doesn't type-check, because `next'` is not a subpattern of the clause pattern of `go`. But this is a less pressing problem. ```juvix go {A B} (f : A -> B) : List A -> List B | nil := nil | (elem :: next) := let var1 := f elem; var2 (next' : List A) : List B := go f next'; in myCons var1 (var2 next); ```		2024-11-15 12:30:18 +01:00
..
Negative.hs	Fix typos (#2573)	2024-01-08 13:27:18 +01:00
Positive.hs	Detect termination for nested local definitions (#3169)	2024-11-15 12:30:18 +01:00