From fc7c1d105390dbc47e2ff36d4d2dd3b60defe48e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jun 2022 17:37:10 -0700 Subject: [PATCH] chore: remove unnecessary `set_option` --- src/Init/System/IO.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 69c437031f..1e62b8e42d 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -665,13 +665,12 @@ universe u namespace Lean -set_option linter.unusedVariables.funArgs false in /-- Typeclass used for presenting the output of an `#eval` command. -/ class Eval (α : Type u) where -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval` -- so that `()` output is hidden in chained instances such as for some `IO Unit`. -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`) - eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit + eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit instance [ToString α] : Eval α where eval a _ := IO.println (toString (a ()))