Module Expr_intf

module Expr_intf: sig .. end

Mcsat expressions

This modules defines the required implementation of expressions for Mcsat.

type negated = Formula_intf.negated =

`\|`	`Negated`	`(*`	changed sign	`*)`
`\|`	`Same_sign`	`(*`	kept sign	`*)`

This type is used during the normalisation of formulas. See Expr_intf.S.norm for more details.

module type S = sig .. end