module FStar.Pervasives

fsdoc: no-summary-found

fsdoc: no-comment-found

let ((expect_failure (errs:list int)):unit):()

When attached a top-level definition, the typechecker will succeed * if and only if checking the definition results in an error. The * error number list is actually OPTIONAL. If present, it will be * checked that the definition raises exactly those errors in the * specified multiplicity, but order does not matter.

let ((expect_lax_failure (errs:list int)):unit):()

When --lax is present, we the previous attribute since some definitions * only fail when verification is turned on. With this attribute, one can ensure * that a definition fails while lax-checking too. Same semantics as above, * but lax mode will be turned on for the definition.

let (tcdecltime:unit):()

Print the time it took to typecheck a top-level definition

let (assume_strictly_positive:unit):()

• THIS ATTRIBUTE IS AN ESCAPE HATCH AND CAN BREAK SOUNDNESS
• USE WITH CARE
• The positivity check for inductive types stops at abstraction
• boundaries. This results in spurious errors about positivity,
• e.g., when defining types like type t = ref (option t)
• By adding this attribute to a declaration of a top-level name
• positivity checks on applications of that name are admitted.
• See, for instance, FStar.Monotonic.Heap.mref
• We plan to decorate binders of abstract types with polarities
• to allow us to check positivity across abstraction boundaries
• and will eventually remove this attribute.

let (unifier_hint_injective:unit):()

• This attribute is to be used as a hint for the unifier.
• A function-typed symbol t marked with this attribute
• will be treated as being injective in all its arguments
• by the unifier.
• That is, given a problem t a1..an =?= t b1..bn
• the unifier will solve it by proving ai =?= bi for
• all i, without trying to unfold the definition of t.

let ((strict_on_arguments (x:list int)):unit):()

• This attribute is used to control the evaluation order
• and unfolding strategy for certain definitions.
• In particular, given
• [@(strict_on_arguments [1;2])]
• let f x0 (x1:list x0) (x1:option x0) = e
• An application f e0 e1 e2 is reduced by the normalizer by:
• 1. evaluating e0 ~>* v0, e1 ~>* v1, e2 ~>* v2
• 2 a.

• If, according to the positional arguments [1;2], 

• if v1 and v2 have constant head symbols 

•        (e.g., v1 = Cons _ _ _, and v2 = None _)

• then `f` is unfolded to `e` and reduced as

•   e[v0/x0][v1/x1][v2/x2]

• 2 b.
• Otherwise, f is not unfolded and the term is f e0 e1 e2
• reduces to f v0 v1 v2.

let (erasable:unit):()

• This attribute can be added to an inductive type definition,
• indicating that it should be erased on extraction to unit.
• However, any pattern matching on the inductive type results
• in a Ghost effect, ensuring that computationally relevant
• code cannot rely on the values of the erasable type.
• See examples/micro-benchmarks/Erasable.fst, for examples.
• Also see https://github.com/FStarLang/FStar/issues/1844