Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replicate
/
.
/
tests
/
lean
/
679.lean
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