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

Equations

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

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

Equations

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

@[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

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