Marking Nodes As Proven/Unprovable/Irrelevant #
Irrelevant #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Proven #
Equations
Instances For
Equations
- r.isProvenNoCache = Array.allM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isProven) r.children
Instances For
Equations
- c.isProvenNoCache = Array.anyM (fun (cref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isProven) c.goals
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Unprovable #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- r.isUnprovableNoCache = Array.anyM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isUnprovable) r.children
Instances For
Equations
- c.isUnprovableNoCache = Array.allM (fun (cref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isUnprovable) c.goals
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Uncached Node States #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.