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

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

@[reducible, inline]

abbrev Std.Tactic.Do.MGoalEntails {σs : List Type} (P Q : Do.SPred σs) : Prop

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

def Std.Tactic.Do.MGoalHypMarker {σs : List Type} (_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.