Index of types

attributes, with a specific case for a source location

A function of type check_term comprises a RAC engine.

The result of a classification based on normal and giant-step RAC execution is comprised of a verdict itself and the log of the relevant execution.

The possible "clone" substitution elements

A comparator for values of type 'a *

A contradiction context carries all necessary information about a contradiction (with snapshot'ed values).

Used to give colors to the parts of the source code that corresponds to the following property in the current task.

Reduce a term (for RAC or for computing ghost expressions).

Binary operators

Bitvectors

Constants

Floats

Fractions

Function arguments and body

Function literal value

Integers

Quantifiers

Concrete term

A configuration linked to an rc file.

constructor symbol with the list of projections

The execution context

top-level declarations

The type of set elements.

enumeration: zipper style

The parts of the execution environment in Pinterp which are relevant for Rac.

An exception match branch

Expressions, equipped with a source location

Expression kinds

A family of parameterized sections in a configuration file.

record fields

filter prover

(fn : 'a format_parser) env path file ch parses the in_channel ch and returns the language-specific contents of type 'a.

formatted: string which is formatted "@ " allow to cut the line if too long

Local function definition

Global information known when server process has started and that can be shared with the IDE through communication

identifiers, with attributes and a source location

A single declaration of an inductive predicate

The type of the map keys.

A single declaration of a function or predicate

Arguments of "meta" declarations

Counter-example model elements.

Parses the input string (i.e.

In order to interpret, that is type, string arguments as symbols or terms, a transformation may need a naming_table.

An oracle provides values during execution in Pinterp for program parameters and during giant steps.

An oracle to get all-quantified variables during RAC.

parameter as 4-uple (loc,id,ghost,type) to represent "ghost? id? : type".

Patterns, equipped with a source location

Normal postconditions

Precondition

a user-created type of unregistered identifiers

The premises during RAC, i.e.

A printer receives a printer_args which is created from the information contained in the driver file.

The marked printer potentially adds the marker, the closed printer adds parentheses to the potentially marked node

The printing info is collected while printing a task to trace back elements in the output of the printer to elements in the task and the AST.

record of necessary data for a given external prover

Type that represents a single prover run

type expressions

qualified identifiers

RAC is defined by a single function Pinterp_core.check_term.

The result state of a RAC execution

A regular match branch

An execution may terminate normally, with an exception, or with an irreducible expression.

A section in a configuration file.

A family of sections without parameters.

Contract

The type of precompiled regular expressions for parsing of steps

A parsed configuration file.

Private Hashtbl

The type of sets of type elt.

The type of maps from type key to type 'a.

a set of coercions

Terms, equipped with a source location

theories under constructions

The type of precompiled regular expressions for time parsing

Type definition body

Variant for both loops and recursive functions.

tau * (tau -> tau -> prop)

Verdict of the classification.

warning identifiers

The configuration of the prover used for reducing terms in RAC

Exceptional postconditions