Hello Abhishek,
The Why3 API for building terms, theories and proof tasks is designed to
forbid the construction of ill-typed terms. This includes a protection
against dangerous traps such as variable name capture. It means that you
can never assume that a logic variable is uniquely
Hello
I have to quantify over a variable in a term, but I only have the term and
the variable name (string). How can I create the corresponding vsymbol to
pass to `t_forall_close`. Is there a function to get the vsymbol of a
particular name in a term?
eg.
enclose (name: string) (t: Term) = (*
Hello
I am trying to use Why3 from Ocaml. I have been looking at API from `
http://why3.lri.fr/doc-0.81/manual005.html`. Below is a piece of code which
should work according to the documentation, but it gives error,
create_theory returns `Why3.Theory.theory_uc` but to make a `lsymbol` I
need
