new syntax of why3 doc

parent 92ac4450
(** {1 Constructive existence of a witness}
Given a predicate [p] over integers and the existence of
a nonnegative integer [n] such that [p n], one can build
Given a predicate `p` over integers and the existence of
a nonnegative integer `n` such that `p n`, one can build
a witness using a linear search starting from 0.
The difficulty here is to prove the termination of the
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment