FStar_Mul needed in fstar.lib

[mtzguido]

Inlining sometimes fails to inline FStar.Mul.op_Star into Prims.op_Multiply, so it shows up in the OCaml. E.g.

module X

open FStar.Mul

unfold let pow2_norm (n:nat) = normalize_term (pow2 n)

let f (x:nat) = pow2_norm (2 * x)

$ ./bin/fstar.exe X.fst --codegen OCaml --extract '-*,X' --cache_off
Extracted module X
Verified module: X
All verification conditions discharged successfully
$ cat X.ml
open Prims
let (pow2_norm : Prims.nat -> Prims.pos) =
  fun n ->
    match n with
    | uu___ when uu___ = Prims.int_zero -> Prims.int_one
    | uu___ -> (Prims.of_int (2)) * (Prims.pow2 (n - Prims.int_one))
let (f : Prims.nat -> Prims.pos) =
  fun x ->
    match (Prims.of_int (2)) * x with
    | uu___ when uu___ = Prims.int_zero -> Prims.int_one
    | uu___ ->
        (Prims.of_int (2)) *
          (Prims.pow2
             ((FStar_Mul.op_Star (Prims.of_int (2)) x) - Prims.int_one))

This is because pow2 gets unfolded to a match with a scrutinee of 2 * x, which is blocked, and we disable delta when we descend into the branches.

This works now since FStar_Mul is in fstar.lib. Mostly posting this to document it.

Ideally this would just be a notation and the entire FStar_Mul module would be noextract.