Documentation

Lean.Util.Sorry

Equations
Instances For
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Equations
                • d.hasNonSyntheticSorry = (d.foldExprM (fun (r : Bool) (e : Lean.Expr) => r || e.hasNonSyntheticSorry) false).run
                Instances For