max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove Inhabited instance

Browse source
This commit is contained in:
Wojciech Nawrocki 2023-01-13 16:27:33 -05:00 • committed by Gabriel Ebner
parent c784031dd7
commit ae97ae35e9
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Widget/InteractiveGoal.lean
View file

@ -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