I stumbled at the following problem when trying to make deeply embedded toy language:
exp, but also for evaluating
Because of the nature of
1) both of them are recursive
2) both of them are mutually recursive
evals is defined locally (using
let statement inside
eval's function definition), recursion is not allowed.
There is a message saying that
evals is not recognized:
Error: The reference evals was not found in the current environment.
How would you overcome this?
you could define evals using
fix, but it's simpler to write
evals ls as
map eval ls
Essentially that error doesn't mean "recursion is not allowed" but "you have not enabled recursion"... Just like Definition does not enable recursion while Fixpoint does.
@Paolo Giarrusso Thanks for the help :+1:
I didn't know
fix existed and didn't consider
map at all -- will try with map first.
Regarding other comment -- I meant to say that having (for example) following function is not possible:
Fail Fixpoint f1 (n1 : nat) := let f2 (n2 : nat) := match n2 with | 0 => f1 0 | S (n2') => f2 n2' end in match n1 with | 0 => 0 | S (n1') => 1 + f2 n1' end.
Since it seems to me (based on the error message) that recursive references inside local function such as f2 are not permitted.
Indeed let (like definition) does not enable recursion, but that's what fix is for. Fixpoint is mostly just a Definition that uses fix.
Thanks again for clarifications :smile:
fold_left did the job in my case.
Nikola Katić has marked this topic as resolved.
Last updated: Sep 30 2023 at 05:01 UTC