kdrag.kernel.consider

kdrag.kernel.consider(x: ExprRef) → None

The purpose of this is to seed the solver with interesting terms. Axiom schema. We may give a fresh name to any constant. An “anonymous” form of define. Pointing out the interesting terms is sometimes the essence of a proof.