Dear all,
I am new to Fstar and theorem provers.
Is there some way to prove a program which looks like this:
----------------------------------------------------------------
module T
let canWrite (f:string) =
match f with
| "demo/tempfile" -> true
| _ -> false
let _ = assert (forall x. canWrite(String.concat "/" ["temp", x]) = false)
----------------------------------------------------------------
I get:
(Warning 271) Pattern uses these theory symbols or terms that should
not be in an smt pattern: Prims.op_Subtraction 1 (see also
/home/arun/.opam/default/lib/fstar/FStar.UInt.fst(671,8-671,51))
... lots of warnings ..., and finally:
T.fst(8,59-8,63): (Error 54) (*?u4*) _ * (*?u5*) _ is not a subtype of
the expected type Prims.string
1 error was reported (see above)
Thank you and regards,
Arun
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
