app package:what4

Type App e tp encodes the top-level application of an Expr expression. It includes first-order expression forms that do not bind variables (contrast with NonceApp). Parameter e is used everywhere a recursive sub-expression would go. Uses of the App type will tie the knot through this parameter. Parameter tp indicates the type of the expression.

This module defines datastructures that encode the basic syntax formers used in What4.ExprBuilder.

Check if two applications are equal.

Apply a set of arguments to a symbolic function.

This either returns the root exactly, or it computes the closest double precision approximation of the root. Underneath the hood, this uses rational arithmetic to guarantee precision, so this operation is relatively slow. However, it is guaranteed to provide an exact answer. If performance is a concern, there are faster algorithms for computing this.

This type represents Expr values that were built from an App. Parameter t is a phantom type brand used to track nonces. Selector functions are provided to destruct AppExpr values, but the constructor is kept hidden. The preferred way to construct an Expr from an App is to use sbMakeExpr.

The theory that a symbol belongs to.

AppPPExpr represents a an application, and it may be let bound.

A doc that can be let bound.