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

chore: fix test

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-08-05 00:13:01 -04:00 • committed by Leonardo de Moura
parent 3bbf19a404
commit 1b44768697
1 changed files with 15 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
tests/lean/run/toFromJson.lean
View file

@ -95,14 +95,20 @@ deriving ToJson, FromJson, Repr, BEq
#eval checkRoundTrip (ERec.mk 7)
#eval checkRoundTrip (ERec.W (ERec.mk 8))
inductive ENest (α : Type)
| mk : Nat → ENest α
| W : (Array (ENest α)) → ENest α
inductive ENest
| mk : Nat → ENest
| W : (Array ENest) → ENest
deriving ToJson, FromJson, Repr, BEq
-- TODO(WN): workaround for elab bug, remove later
def ENest.mk' : Nat → ENest Nat :=
ENest.mk (α := Nat)
#eval checkToJson (ENest.W #[ENest.mk' 9]) (json { W : [{ mk : 9 }]})
#eval checkRoundTrip (ENest.mk' 10)
#eval checkRoundTrip (ENest.W #[ENest.mk' 11])
#eval checkToJson (ENest.W #[ENest.mk 9]) (json { W : [{ mk : 9 }]})
#eval checkRoundTrip (ENest.mk 10)
#eval checkRoundTrip (ENest.W #[ENest.mk 11])
inductive EParam (α : Type)
| mk : α → EParam α
deriving ToJson, FromJson, Repr, BEq
#eval checkToJson (EParam.mk 12) (json { mk : 12 })
#eval checkToJson (EParam.mk "abcd") (json { mk : "abcd" })
#eval checkRoundTrip (EParam.mk 13)
#eval checkRoundTrip (EParam.mk "efgh")