Hey Clément, a small bugfix arising from a report in our public Slack. The commit message below explains.
This flag is meant for extraction, and prevents the reduction of pure
letbindings such as let x = 1 in 2. The funny thing is that F* will
call Normalize.term_to_string before giving the printed term
back to fstar-mode, so this is not that easy to trigger.
With this snippet, however:
val tail_fib : nat -> (int * int)
let rec tailfib n = match n with
| 0 -> (0, 0)
| 1 -> (1, 0)
| -> let (n1, n2) = tail_fib (n-1) in (n1 + n2, n1)
Hey Clément, a small bugfix arising from a report in our public Slack. The commit message below explains.
This flag is meant for extraction, and prevents the reduction of pure letbindings such as
let x = 1 in 2
. The funny thing is that F* will call Normalize.term_to_string before giving the printed term back to fstar-mode, so this is not that easy to trigger.With this snippet, however:
val tail_fib : nat -> (int * int) let rec tailfib n = match n with | 0 -> (0, 0) | 1 -> (1, 0) | -> let (n1, n2) = tail_fib (n-1) in (n1 + n2, n1)
let fib2 n = let a, b = tail_fib n in a
Evaluating
fib2 4
actually givesfib2 4 ↓βδιζrp 1 + 0 + 1 + (1 + 0) <: int