From fdce66151f71303e2c700e645491aa13c940af84 Mon Sep 17 00:00:00 2001 From: Andrii Kurdiumov Date: Sun, 7 Aug 2022 17:50:45 +0600 Subject: [PATCH] Add clarification Without `open FStar.Mul` complete novice would struggle to understand why perfectly valid example does not work in sandbox. --- doc/book/code/Vec.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/book/code/Vec.fst b/doc/book/code/Vec.fst index 031781e5c0e..699a3f8d3d5 100644 --- a/doc/book/code/Vec.fst +++ b/doc/book/code/Vec.fst @@ -118,9 +118,9 @@ let rec foldr #a #n #acc f hd (foldr f tl init) //SNIPPET_END: foldr +//SNIPPET_START: norm_spec open FStar.Mul -//SNIPPET_START: norm_spec let rec pow2 (n:nat) : nat = if n = 0 then 1 else 2 * pow2 (n - 1)