We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
ToJson
FromJson
String.Slice
1 parent b2c058f commit 8ada38eCopy full SHA for 8ada38e
src/Lean/Data/Json/FromToJson/Basic.lean
@@ -46,6 +46,8 @@ instance : FromJson Int := ⟨Json.getInt?⟩
46
instance : ToJson Int := ⟨fun n => Json.num n⟩
47
instance : FromJson String := ⟨Json.getStr?⟩
48
instance : ToJson String := ⟨fun s => s⟩
49
+instance : FromJson String.Slice := ⟨Except.map String.toSlice ∘ Json.getStr?⟩
50
+instance : ToJson String.Slice := ⟨fun s => s.copy⟩
51
52
instance : FromJson System.FilePath := ⟨fun j => System.FilePath.mk <$> Json.getStr? j⟩
53
instance : ToJson System.FilePath := ⟨fun p => p.toString⟩
0 commit comments