From ae97ae35e9fca284782bbd8917781afd30926b5f Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 13 Jan 2023 16:27:33 -0500 Subject: [PATCH] chore: remove Inhabited instance --- src/Lean/Widget/InteractiveGoal.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index 3492b03975..82025d2bc0 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -43,7 +43,6 @@ structure InteractiveGoalCore where type : CodeWithInfos /-- Metavariable context that the goal is well-typed in. -/ ctx : WithRpcRef Elab.ContextInfo - deriving Inhabited /-- An interactive tactic-mode goal. -/ structure InteractiveGoal extends InteractiveGoalCore where @@ -58,7 +57,7 @@ structure InteractiveGoal extends InteractiveGoalCore where isInserted? : Option Bool := none /-- If true, the goal will be removed on the next tactic state. -/ isRemoved? : Option Bool := none - deriving Inhabited, RpcEncodable + deriving RpcEncodable /-- An interactive term-mode goal. -/ structure InteractiveTermGoal extends InteractiveGoalCore where @@ -66,7 +65,7 @@ structure InteractiveTermGoal extends InteractiveGoalCore where range : Lsp.Range /-- Information about the term whose type is the term-mode goal. -/ term : WithRpcRef Elab.TermInfo - deriving Inhabited, RpcEncodable + deriving RpcEncodable def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String) (goalPrefix : String) : Format := Id.run do