Equations
- x.isSorry = match x with | ((Lean.Expr.const `sorryAx us).app arg).app arg_1 => true | x => false
Instances For
Equations
- x.isSyntheticSorry = match x with | ((Lean.Expr.const `sorryAx us).app arg).app (Lean.Expr.const `Bool.true us_1) => true | x => false
Instances For
Equations
- x.isNonSyntheticSorry = match x with | ((Lean.Expr.const `sorryAx us).app arg).app (Lean.Expr.const `Bool.false us_1) => true | x => false
Instances For
Equations
- e.hasSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isConstOf `sorryAx) e).isSome
Instances For
Equations
- e.hasSyntheticSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isSyntheticSorry) e).isSome
Instances For
Equations
- e.hasNonSyntheticSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isNonSyntheticSorry) e).isSome