Expr

Expr#

Data structuers for expressions and goals

class pantograph.expr.Goal(id: str, variables: list[pantograph.expr.Variable], target: str, sibling_dep: Optional[set[int]] = <factory>, name: Optional[str] = None, mode: pantograph.expr.TacticMode = <TacticMode.TACTIC: 1>)#

class pantograph.expr.GoalState(state_id: int, goals: list[pantograph.expr.Goal], messages: list[pantograph.message.Message], _sentinel: list[int])#

property is_solved: bool#

WARNING: Does not handle dormant goals.

class pantograph.expr.Site(goal_id: int | None = None, auto_resume: bool | None = None)#: Acting area of a tactic

class pantograph.expr.Subsumption(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#: Subsumption result

class pantograph.expr.TacticDraft(expr: str)#: Assigns an expression to the current goal

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.TacticMode(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)#: Current execution mode

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’.

Represent a PEP 604 union type

E.g. for int | str

Expr

Contents

Expr#