Expr

Expr#

Data structuers for expressions and goals

class pantograph.expr.Goal(variables: list[pantograph.expr.Variable], target: str, sibling_dep: list[int] = <factory>, name: Optional[str] = None, is_conversion: bool = False)#
class pantograph.expr.GoalState(state_id: int, goals: list[pantograph.expr.Goal], _sentinel: list[int])#
property is_solved: bool#

WARNING: Does not handle dormant goals.

class pantograph.expr.TacticCalc(step: str)#

The calc tactic, equivalent to `lean calc {step} := ... ` You can use _ in the step.

class pantograph.expr.TacticExpr(expr: str)#

Assigns an expression to the current goal

class pantograph.expr.TacticHave(branch: str, binder_name: str | None = None)#

The have tactic, equivalent to `lean have {binder_name} : {branch} := ... `

class pantograph.expr.TacticLet(branch: str, binder_name: str | None = None)#

The let tactic, equivalent to `lean let {binder_name} : {branch} := ... `

class pantograph.expr.Variable(t: str, v: str | None = None, name: str | None = None)#
pantograph.expr.Expr: TypeAlias = <class 'str'>#

str(object=’’) -> str str(bytes_or_buffer[, encoding[, errors]]) -> str

Create a new string object from the given object. If encoding or errors is specified, then the object must expose a data buffer that will be decoded using the given encoding and error handler. Otherwise, returns the result of object.__str__() (if defined) or repr(object). encoding defaults to sys.getdefaultencoding(). errors defaults to ‘strict’.

pantograph.expr.Tactic: TypeAlias = str | pantograph.expr.TacticHave | pantograph.expr.TacticLet | pantograph.expr.TacticCalc | pantograph.expr.TacticExpr#

Represent a PEP 604 union type

E.g. for int | str

Contents