diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out index baa9dd9475..7922d9a53d 100644 --- a/tests/lean/Reformat.lean.expected.out +++ b/tests/lean/Reformat.lean.expected.out @@ -147,15 +147,6 @@ theorem natAddZero (n : Nat) : n + 0 = n := theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl -/--Like `by applyInstance`, but not dependent on the tactic framework. -/ -@[reducible] -def inferInstance {α : Type u} [i : α] : α := - i - -@[reducible] -def inferInstanceAs (α : Type u) [i : α] : α := - i - @[extern c inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂