Custom error messages.

def termThrowParserError__ : Lean.ParserDescr

Throws an error coming from parsing the optimization problem using the custom syntax defined in CvxLean/Syntax/Minimization.lean.

Equations

• One or more equations did not get rendered due to their size.

def termThrowTacticBuilderError__ : Lean.ParserDescr

Throws an error coming from the tactic builder machinery (CvxLean/Meta/TacticBuilder.lean).

Equations

• One or more equations did not get rendered due to their size.

def termThrowCleanUpCompError__ : Lean.ParserDescr

Throws an error coming from the clean_up_comp tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowChangeOfVariablesError__ : Lean.ParserDescr

Throws an error coming from the change_of_variables tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowConvOptError__ : Lean.ParserDescr

Throws an error coming from the conv_opt tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowConvObjError__ : Lean.ParserDescr

Throws an error coming from the conv_obj tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowConvConstrError__ : Lean.ParserDescr

Throws an error coming from the conv_constr tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRemoveConstrError__ : Lean.ParserDescr

Throws an error coming from the remove_constrs tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRemoveTrivialConstrsError__ : Lean.ParserDescr

Throws an error coming from the remove_trivial_constrs tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRenameConstrsError__ : Lean.ParserDescr

Throws an error coming from the rename_constrs tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRenameVarsError__ : Lean.ParserDescr

Throws an error coming from the rename_vars tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowReorderConstrsError__ : Lean.ParserDescr

Throws an error coming from the reorder_constrs tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRwConstrError__ : Lean.ParserDescr

Throws an error coming from the rw_constr tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRwObjError__ : Lean.ParserDescr

Throws an error coming from the rw_obj tactic.

Equations

• One or more equations did not get rendered due to their size.

def termThrowPreDCPError__ : Lean.ParserDescr

Throws an error coming from the pre_dcp tactic or any of the auxiliary functions.

Equations

• One or more equations did not get rendered due to their size.

def termThrowAtomDeclarationError__ : Lean.ParserDescr

Throws an error coming from the declare_atom command.

Equations

• One or more equations did not get rendered due to their size.

def termThrowDCPError__ : Lean.ParserDescr

Throws an error coming from the dcp tactic or any of the auxiliary functions.

Equations

• One or more equations did not get rendered due to their size.

def termThrowCoeffsError__ : Lean.ParserDescr

Throws an error coming from the coefficient extraction procedure (CvxLean/Command/Solve/Float/Coeffs.lean).

Equations

• One or more equations did not get rendered due to their size.

def termThrowRealToFloatError__ : Lean.ParserDescr

Throws an error coming from the real-to-float procedure (CvxLean/Command/Solve/Float/RealToFloatCmd.lean).

Equations

• One or more equations did not get rendered due to their size.

def termThrowSolveError__ : Lean.ParserDescr

Throws an error coming from the solve command.

Equations

• One or more equations did not get rendered due to their size.

def termThrowEquivalenceError__ : Lean.ParserDescr

Throws an error coming from the equivalence command.

Equations

• One or more equations did not get rendered due to their size.

def termThrowReductionError__ : Lean.ParserDescr

Throws an error coming from the reduction command.

Equations

• One or more equations did not get rendered due to their size.

def termThrowRelaxationError__ : Lean.ParserDescr

Throws an error coming from the relaxation command.

Equations

• One or more equations did not get rendered due to their size.