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 62f2f92 commit d585d5bCopy full SHA for d585d5b
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