lean_dojo.interaction.parse_goals

Utilities for parsing Lean’s pretty-printed proof goals.

class lean_dojo.interaction.parse_goals.Declaration(ident: str, lean_type: str)

Bases: object

A declaration in the local context.

ident: str

lean_type: str

class lean_dojo.interaction.parse_goals.Goal(assumptions: List[Declaration], conclusion: str)

Bases: object

A goal in Lean.

assumptions: List[Declaration]

conclusion: str

classmethod from_pp(pp: str) → Goal

Parse a pretty-printed goal.

lean_dojo.interaction.parse_goals.parse_goals(pp: str) → List[Goal]

Parse a list of pretty-printed goals.