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

fix: rm instance TypeName String because it is unused

Browse source
This commit is contained in:
E.W.Ayers 2022-09-30 10:21:44 +01:00 • committed by Leonardo de Moura
parent 7f8c45b6f3
commit 7c8fcb3233
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Deriving/TypeName.lean
View file

@ -23,6 +23,3 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
initialize
registerDerivingHandler ``TypeName deriveTypeNameInstance
deriving instance TypeName for String
instance : Inhabited Dynamic := ⟨Dynamic.mk ""⟩