Documentation

Lifted expressions for pattern match checking.

Literals (simple and overloaded ones) for pattern match checking.

Represents a match against a literal. We mostly use it to to encode shapes for a variable that immediately lead to a refutation.

See Note [Refutable shapes] in TmOracle. Really similar to AltCon.

A term constraint. TVC x e encodes that x is equal to e.

Equality between literals for pattern match checking.

Check if an expression is lifted or not