blob: 80fe3766103baea8fa543b52a679751dc30791ba [file] [edit]
import Lean
open Lean
def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
let json := toJson x
fromJson? json
#eval encodeDecode Name.anonymous