Variable defined by "where" sometimes "not found in the current environment"

[mattam82]

Variable defined by "where" sometimes "not found in the current environment"

[anton-trunov]

I guess I hit the same issue.

The following works:

Equations foo (n : nat) : nat :=
foo n := bar (S n)
where bar (n : nat) : nat :=
bar n := n.

This snippet

Equations foo (n : nat) : nat :=
foo n := bar (S n)
where bar (n : nat) : nat :=
bar O := O;
bar (S n) := bar n.

produces the following error message:

Error: The variable bar was not found in the current environment.

pointing to the bar (S n) := bar n. clause as the source of the error.

When adding curly braces like so

Equations foo (n : nat) : nat := {
foo n := bar (S n) }
where bar (n : nat) : nat :=
bar O := O;
bar (S n) := bar n.

the error message stays the same, but this time the line that gets marked as the source is foo n := bar (S n) }.

[mattam82]

I think you should put braces around the bar clauses to avoid this. Le mar. 1 mai 2018 à 16:04, Anton Trunov <[email protected]> a écrit :

…

I guess I hit the same issue. The following works: Equations foo (n : nat) : nat := foo n := bar (S n)where bar (n : nat) : nat := bar n := n. This snippet Equations foo (n : nat) : nat := foo n := bar (S n)where bar (n : nat) : nat := bar O := O; bar (S n) := bar n. produces the following error message: Error: The variable bar was not found in the current environment. pointing to the bar (S n) := bar n. clause as the source of the error. When adding curly braces like so Equations foo (n : nat) : nat := { foo n := bar (S n) }where bar (n : nat) : nat := bar O := O; bar (S n) := bar n. the error message stays the same, but this time the line that gets marked as the source is foo n := bar (S n) }. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#79 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARYOkEt07eAxYreT-NHov_VLvGtkuks5tuGt4gaJpZM4TqdHW> .

[anton-trunov]

I've tried that, it didn't work:

Equations foo (n : nat) : nat := {
foo n := bar (S n) }
where bar (n : nat) : nat := {
bar O := O;
bar (S n) := bar n }.

[anton-trunov]

It only works if bar mentiones foo:

Equations foo (n : nat) : nat := {
foo n := bar n }
where bar (n : nat) : nat := {
bar O := O;
bar (S n) := foo n }.

However, if I remove the braces it fails again:

Fail Equations foo (n : nat) : nat := 
foo n := bar n
where bar (n : nat) : nat :=
bar O := O;
bar (S n) := foo n.

[mattam82]

Interesting... there is a syntactic check indeed for recursion Le mar. 1 mai 2018 à 16:27, Anton Trunov <[email protected]> a écrit :

…

It only works if bar mentiones foo: Equations foo (n : nat) : nat := { foo n := bar n }where bar (n : nat) : nat := { bar O := O; bar (S n) := foo n }. However, if I remove the braces it fails again: Fail Equations foo (n : nat) : nat := foo n := bar nwhere bar (n : nat) : nat := bar O := O; bar (S n) := foo n. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#79 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARZwXuke6BRksAHvinDQM8IqGd533ks5tuHCxgaJpZM4TqdHW> .

[mattam82]

Next on my list, indeed the syntactic check is too crude to determine whether things are mutually recursive or not, I will have to build a dependency graph it seems.

[mattam82]

Actually, these can't be mutually recursive:

Fixpoint foo (n : nat) : nat := 
  bar n
with bar (n : nat) : nat :=
       match n with 0 => 0 | S n => foo n end.

Fails.

[mattam82]

So it's rather that foo is recursive while bar isn't (it's just a definition in this case).

[mattam82]

Also there are examples where you want the where clause itself to be recursive, that requires a few changes as well.

[mattam82]

This now works by specifying "by struct fs" for both "sum" and "sum_aux". The fix is in master and will be part of the upcoming release.