Skip to content

Namespace FStar.Mul cannot be found #54

@JansthcirlU

Description

@JansthcirlU

Hi all, I installed the F* Windows binaries through the latest release, downloading it to C:\Program Files\fstar and adding the bin path to my environment variable. I then started working on the first Sample tutorial and the extension correctly called the fstar executable until I tried to open FStar.Mul to use the * as multiplication.

Here's what my code looks like:

module Sample

let incr (x:int) : int = x + 1
let incr1 (x:int) : y:int{y > x} = x + 1
// let incr2 (x:int) : nat = x + 1
let incr3 (x:nat) : nat = x + 1

val incr4 (x:int{x >= -2}) : y:int{y >= -1}
let incr4 x = x + 1

// Max
val max (x:int) (y:int) : z:int{if x >= y then z = x else z = y}
let max x y = if x >= y then x else y

open FStar.Mul (* - Namespace FStar.Mul cannot be found *)

let rec factorial (n:nat) : nat =
    if n = 0
    then 1
    else n * factorial (n - 1)

But when I manually run fstar Sample.fst, code verification happens without errors.

What could the problem be and how could I resolve it?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions