meta

Expr

data Expr

First-order reflection of terms seen by tactic programs: de Bruijn variables (0 is the nearest binding), constants and constructors by name (a constructor’s parameters are left out), and opaque for what the reflection cannot read.

Expr.applyBool

def applyBool (name : String) (operands : List Bool) : Option Bool

A Boolean operator applied to the values of its operands: Bool.not to one, Bool.and and Bool.or to two.

Expr.boolValue

def boolValue (e : Expr) : Option Bool

The value of an expression built from true, false, not, and and or; nothing for anything else.

Expr.decideBool

def decideBool (goal : Expr) : Option Expr

For a goal lhs = rhs between Boolean expressions with the same value: the constant path to the right side.