source
def Std.Tactic.Do.mgoalHyp :
Lean.ParserDescr
Equations

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

Instances For

source
def Std.Tactic.Do.mgoalStx :
Lean.ParserDescr
Equations

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

Instances For

source
@[reducible, inline]
abbrev Std.Tactic.Do.MGoalEntails {σs : List (Type u_1)} (P Q : Do.SPred σs) :
Prop

This is the same as `SPred.entails`. This constant is used to detect `SPred` proof mode goals.

Equations

- @Std.Tactic.Do.MGoalEntails = @Std.Do.SPred.entails

Instances For

source
def Std.Tactic.Do.MGoalHypMarker {σs : List (Type u)} (_A : Do.SPred σs) :
Prop

This is only used for delaboration purposes, so that we can render context variables that appear to have type `A : PROP` even though `PROP` is not a type.

Equations

- _A = True

Instances For