kdrag.kernel.define

kdrag.kernel.define(name: str, args: list[ExprRef], body: ExprRef) → FuncDeclRef

Define a non recursive definition. Useful for shorthand and abstraction. Does not currently defend against ill formed definitions. TODO: Check for bad circularity, record dependencies

Parameters:

• name – The name of the term to define.

• args – The arguments of the term.

• defn – The definition of the term.

Returns:

A tuple of the defined term and the proof of the definition.

Return type:

tuple[smt.FuncDeclRef, __Proof]