Checker "rpylean"
Version: v2026.4.1 · 📄 Declaration · 🔗 Source
rpylean - A Lean type checker written in (R)Python.
88/96
44/45
0
Detailed results
Test "bogus1"
Expected: ✋ reject · Size: 11.4 KB · Lines: 198 · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
A clearly bogus proof. Also serves as an example for how to write simple cases.
Test result: ✋ rejected · exit code 1 · wall time: 13 ms · instructions: 20.6 M · max rss memory: 6.8 MB
stderr:
theorem thm : Eq (OfNat.ofNat 0) (OfNat.ofNat 1) := True.intro
^^^^^^^^^^
has type
True
but is expected to have type
Eq (OfNat.ofNat 0) (OfNat.ofNat 1)
parsed in 0.001539s, checked in 0.000606s
Test "cedar"
Expected: 👍 accept · Size: 728.6 MB · Lines: 13.4 M · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 Declaration · 🔗 Source
Lean formalization of, and proofs about, Cedar.
Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.
This test case exports the whole Cedar module and as such contains even unused parts Init and
Batteries.
Test result: ✋ rejected · exit code 1 · wall time: 40.1 s · instructions: 258.1 G · max rss memory: 14.1 GB
stdout:
WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff73007a0> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> WARNING: W_App.try_iota_reduce: unimplemented case num_motives != 1 for <Name object at 0x7ffff72e4890> Building large nat expr for <rbigint object at 0x555603c1c3f8>
stderr:
def DecidableRel.{u, v} : {α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max (max 1 u) v) :=
fun {α β} r ↦ (a : α) → (b : β) → Decidable (r a b)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
has type
{α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max u (max v 1))
but is expected to have type
{α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max (max 1 u) v)
Test "constlevels"
Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.0-rc2 · 📄 Declaration
Regression test for undefined behavior in lazy_delta_reduction_step in the official kernel
In the function lazy_delta_reduction_step, the official kernel expects unfold_definition
to always succeed. However, if the constant has an incorrect number of level parameters, it
actually fails, which leads to memory corruption in lazy_delta_reduction_step.
This test is to check that the official kernel and also other kernels that closely follow the logic of the official kernel correctly handle this unfolding failure.
The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577.
Test result: ✋ rejected · exit code 1 · wall time: 187 ms · instructions: 22.8 M · max rss memory: 7.2 MB
stderr:
RPython traceback: File "rpylean_objects.c", line 31508, in W_Declaration_type_check File "rpylean_objects_1.c", line 10283, in W_Theorem_type_check File "rpylean_objects.c", line 8408, in W_Let_infer Fatal RPython error: AssertionError
Test "cslib"
Expected: 👍 accept · Size: 1.2 GB · Lines: 22.8 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The Lean Computer Science Library (CSLib).
Test result: ✋ rejected · exit code 1 · wall time: 30.4 s · instructions: 249.6 G · max rss memory: 5.7 GB
stdout:
Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e07298> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e07298> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x5556835a3010> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e07298> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e07298> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x555671d0d808> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0> Building large nat expr for <rbigint object at 0x7ffff6e072b0>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 120, in CLI_main ... Fatal RPython error: RuntimeError
Test "init"
Expected: 👍 accept · Size: 309.5 MB · Lines: 6.1 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The Init module export from Lean 4 core.
This test contains the fundamental building blocks of Lean 4, including:
- Basic data types (Nat, List, Array, String, etc.)
- Core tactics and syntax
- Foundational mathematical structures
- Essential metaprogramming infrastructure
This is one of the smallest meaningful test cases, making it ideal for initial checker validation and debugging.
Test result: ✋ rejected · exit code 1 · wall time: 2.3 m · instructions: 699.6 G · max rss memory: 14.1 GB
stderr:
def DecidableRel.{u, v} : {α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max (max 1 u) v) :=
fun {α β} r ↦ (a : α) → (b : β) → Decidable (r a b)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
has type
{α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max u (max v 1))
but is expected to have type
{α : Sort u} → {β : Sort v} → (∀ (a : α), ∀ (a : β), Prop) → Sort (max (max 1 u) v)
Test "init-prelude"
Expected: 👍 accept · Size: 3.5 MB · Lines: 63.7 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The Init.Prelude module export.
Test result: ✋ rejected · exit code 1 · wall time: 1.7 s · instructions: 12.3 G · max rss memory: 251.3 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa488> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa488> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x55555e0520e0> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa488> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa488> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff60480b0> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470> Building large nat expr for <rbigint object at 0x7ffff74aa470>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 120, in CLI_main ... Fatal RPython error: RuntimeError
Test "level-imax-leq"
Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration
Proof of False via incorrect universe level comparison for imax.
A correct kernel must reject leq(imax(u,v)+1, imax(u,v)), since at u=0, v=0 this becomes
leq(1, 0) which is false. However, a checker that only compares the imax arguments
structurally (without accounting for an accumulated successor offset) will incorrectly accept it.
This allows defining a universe-collapsing identity function
down.{u,v} : Sort (succ (imax u v)) → Sort (imax u v), which is used to cast between
True and False via Bool.rec at Sort (imax 0 0) = Prop.
Nanoda incorrectly accepted this proof until it was fixed.
Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 12.2 M · max rss memory: 6.5 MB
stderr:
def down.{u, v} : Type (imax u v) → Sort (imax u v) :=
fun x ↦ x
^^^^^^^^^
has type
Type (imax u v) → Type (imax u v)
but is expected to have type
Type (imax u v) → Sort (imax u v)
parsed in 0.000758s, checked in 0.000137s
Test "level-imax-normalization"
Expected: ✋ reject · Size: 5.8 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 Declaration
Proof of False via incorrect universe level normalization for imax.
A correct kernel must distinguish imax 0 v from succ(imax 0 v), since at v=0 these
evaluate to 0 and 1 respectively. However, a level normalization algorithm that drops an
accumulated successor offset when decomposing imax u (param v) will produce identical normal
forms for both, causing the equivalence check to incorrectly return true.
This allows defining a universe-collapsing identity function
down.{v} : Sort (succ (imax 0 v)) → Sort (imax 0 v), and then
myProp : Prop := down.{0} Bool (a Prop that is computationally Bool). Proof irrelevance on
myProp equates Bool.true and Bool.false, and Bool.rec maps this into False.
Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 12.1 M · max rss memory: 6.5 MB
stderr:
def down.{v} : Type v → Sort v :=
fun x ↦ x
^^^^^^^^^
has type
Type v → Type v
but is expected to have type
Type v → Sort v
parsed in 0.000655s, checked in 0.000123s
Test "mathlib"
Expected: 👍 accept · Size: 5.2 GB · Lines: 100.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The complete Mathlib library export.
This test contains all the mathematical definitions, theorems, and proofs from Mathlib, representing the largest and most comprehensive test case in the Lean kernel arena.
Test result: ✋ rejected · exit code 1 · wall time: 1.8 m · instructions: 766.8 G · max rss memory: 14.1 GB
Test "mlir"
Expected: 👍 accept · Size: 28.8 MB · Lines: 576.3 k · lean4export: 3.1.0 · Lean: 4.27.0-nightly-2025-12-01 · 📄 Declaration · 🔗 Source
The main theorems from lean-mlir.
Test result: ✋ rejected · exit code 1 · wall time: 3.3 s · instructions: 23.4 G · max rss memory: 480.8 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a380> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a380> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x55556d82cad0> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a380> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a380> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x555570ca6a10> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368> Building large nat expr for <rbigint object at 0x7ffff729a368>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 120, in CLI_main ... Fatal RPython error: RuntimeError
Test "nat-rec-rules"
Expected: ✋ reject · Size: 8.2 KB · Lines: 128 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 Declaration
Proof of False via incorrect recursor rule validation.
When processing an inductive type declaration, a correct kernel must verify that the generated recursor rules match the ones provided in the export data. A checker that accidentally compares the imported rules against themselves (instead of against independently constructed rules) will accept arbitrary recursor reduction behavior.
This test defines Nat with a wrong Nat.rec succ rule that always returns hzero (ignoring
the induction hypothesis). Combined with a nat literal extension that hardcodes correct
arithmetic for concrete nat literals but falls back to the wrong Nat.rec rules for symbolic
arguments, this creates an inconsistency that yields a proof of False.
Nanoda incorrectly accepted this proof until it was fixed.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000605s, checked in 0.000071s
Test "perf/app-lam"
Expected: 👍 accept · Size: 1.2 MB · Lines: 28.6 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
A synthetically generated term with n levels of alternating applications and lambdas, with DAG sharing.
At each level, a constant is applied to two identical lambda arguments. The export format records these as a single shared expression (DAG). Each lambda body grows with the nesting depth, referencing all enclosing binders.
This tests two aspects of checker performance:
Infer cache: Since both arguments at each level are the same expression, a checker without an infer cache re-infers the type of each shared subterm, doubling work at every level — O(2ⁿ) total.
Substitution cost: Even with a cache, type-inferring each lambda requires substituting into its body (size O(n)) at each of the n levels, giving O(n²) total. Whether this cost arises depends on the checker's binder representation.
Test result: 👍 accepted · exit code 0 · wall time: 28 ms · instructions: 248.2 M · max rss memory: 18.6 MB
stderr:
parsed in 0.019402s, checked in 0.000805s
Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
A grind tactic test from the Lean 4 test suite.
This produces a theorem with a rather large proof term that needs fast reduction.
Test result: ✋ rejected · exit code 1 · wall time: 1.7 s · instructions: 13.2 G · max rss memory: 278.6 MB
stdout:
Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x55555d4e2c50> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635ef8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x55555993c1b8> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10> Building large nat expr for <rbigint object at 0x7ffff7635f10>
stderr:
Unexpected error during type checking RPython traceback: File "implement.c", line 25, in main File "rpylean__rcli.c", line 120, in CLI_main ... Fatal RPython error: RuntimeError
Test "perf/shift-cascade"
Expected: 👍 accept · Size: 256.3 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
Stress test for cascading substitution overhead in kernel let processing.
N nested let bindings inside a lambda, where each value references the
outer lambda parameter and the previous binding:
fun (a : Nat → Nat) => let f₁ := fun x => a x let f₂ := fun x => a (f₁ x) ... let fₙ := fun x => a (fₙ₋₁ x) fₙ 0
The kernel processes each let by substituting the value into the body.
Each value has a free bvar (references a), so substitution under inner
binders creates shifted copies. In a de Bruijn kernel with deferred shifts,
these Shift(val, offset) wrappers accumulate: step k must traverse
through O(k) wrappers from previous steps, giving O(N²) total work.
A locally-nameless kernel substitutes fvars that need no shifting, giving O(N) total.
N=1000 in the Lean source. Increase to stress further.
Test result: 👍 accepted · exit code 0 · wall time: 15 ms · instructions: 77.1 M · max rss memory: 14.8 MB
stderr:
parsed in 0.005888s, checked in 0.002468s
Test "std"
Expected: 👍 accept · Size: 526.1 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The complete Std library export from Lean 4.
This test contains the standard library extensions beyond core Lean 4, including:
- Enhanced data structures (HashMap, RBTree, etc.)
- Additional mathematical operations
- Extended list and array operations
- Utility functions and theorems
This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.
Test result: ✋ rejected · exit code 1 · wall time: 3.0 m · instructions: 1.0 T · max rss memory: 14.1 GB
Test "tutorial/001_basicDef"
Expected: 👍 accept · Size: 371 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Basic definition
Test result: 👍 accepted · exit code 0 · wall time: 21 ms · instructions: 18.0 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000810s, checked in 0.000574s
Test "tutorial/002_badDef"
Expected: ✋ reject · Size: 369 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Mismatched types
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
def badDef : Prop :=
Type
^^^^
has type
Type 1
but is expected to have type
Prop
parsed in 0.000303s, checked in 0.000073s
Test "tutorial/003_arrowType"
Expected: 👍 accept · Size: 626 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Arrow type (function type)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000324s, checked in 0.000045s
Test "tutorial/004_dependentType"
Expected: 👍 accept · Size: 464 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Dependent type (forall)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000333s, checked in 0.000041s
Test "tutorial/005_constType"
Expected: 👍 accept · Size: 901 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda expression
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000308s, checked in 0.000045s
Test "tutorial/006_betaReduction"
Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000316s, checked in 0.000082s
Test "tutorial/007_betaReduction2"
Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction under binder
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000300s, checked in 0.000045s
Test "tutorial/008_forallSortWhnf"
Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The binding domain of a forall may need to be reduce before it is a sort
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000319s, checked in 0.000041s
Test "tutorial/009_forallSortBad"
Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The binding domain of a forall has to be a sort
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
def forallSortBad : Prop :=
∀ (x : id Prop), ∀ (x : x), x → x
^
has type
x
but is expected to be a Sort (Type or Prop)
parsed in 0.000295s, checked in 0.000082s
Test "tutorial/010_nonTypeType"
Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a declaration has to be a type, not some other expression
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
def nonTypeType : constType :=
^^^^^^^^^
has type
Type → Type → Type
but is expected to be a Sort (Type or Prop)
parsed in 0.000309s, checked in 0.000061s
Test "tutorial/011_nonPropThm"
Expected: ✋ reject · Size: 428 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a theorem has to be a proposition
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
theorem nonPropThm : Prop := ∀ (x : Prop), x
^^^^
has sort
Type
but the type of a theorem must be a proposition (Prop)
parsed in 0.000356s, checked in 0.000067s
Test "tutorial/012_levelComp1"
Expected: 👍 accept · Size: 395 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000292s, checked in 0.000038s
Test "tutorial/013_levelComp2"
Expected: 👍 accept · Size: 413 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000388s, checked in 0.000043s
Test "tutorial/014_levelComp3"
Expected: 👍 accept · Size: 431 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000386s, checked in 0.000040s
Test "tutorial/015_levelParams"
Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level parameters
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000389s, checked in 0.000054s
Test "tutorial/016_tut06_bad01"
Expected: ✋ reject · Size: 431 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Duplicate universe parameters
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 6.1 MB
stderr:
Invalid declaration tut06_bad01.{u, u}: duplicate level parameter u
Test "tutorial/017_levelComp4"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000316s, checked in 0.000048s
Test "tutorial/018_levelComp5"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000345s, checked in 0.000031s
Test "tutorial/019_imax1"
Expected: 👍 accept · Size: 813 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000353s, checked in 0.000047s
Test "tutorial/020_imax2"
Expected: 👍 accept · Size: 832 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000370s, checked in 0.000045s
Test "tutorial/021_inferVar"
Expected: 👍 accept · Size: 717 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference of local variables
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000376s, checked in 0.000052s
Test "tutorial/022_defEqLambda"
Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Definitional equality between lambdas
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000357s, checked in 0.000078s
Test "tutorial/023_peano1"
Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 = 2
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.4 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000452s, checked in 0.000217s
Test "tutorial/024_peano2"
Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 1 + 1 = 2
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.7 M · max rss memory: 6.8 MB
stderr:
parsed in 0.000477s, checked in 0.000280s
Test "tutorial/025_peano3"
Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 * 2 = 4
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.1 M · max rss memory: 6.9 MB
stderr:
parsed in 0.000494s, checked in 0.000349s
Test "tutorial/026_letType"
Expected: 👍 accept · Size: 493 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a non-dependent let
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000344s, checked in 0.000049s
Test "tutorial/027_letTypeDep"
Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a dependent let
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000343s, checked in 0.000061s
Test "tutorial/028_letRed"
Expected: 👍 accept · Size: 631 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing a let
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 10.9 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000304s, checked in 0.000046s
Test "tutorial/029_empty"
Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple empty inductive type
Test result: 👍 accepted · exit code 0 · wall time: 18 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000440s, checked in 0.000026s
Test "tutorial/030_boolType"
Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple enumeration inductive type
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.3 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000412s, checked in 0.000029s
Test "tutorial/031_twoBool"
Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple product type
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.6 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000443s, checked in 0.000037s
Test "tutorial/032_andType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (no level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.5 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000461s, checked in 0.000047s
Test "tutorial/033_prodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.6 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000524s, checked in 0.000050s
Test "tutorial/034_pprodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with more general level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.6 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000503s, checked in 0.000051s
Test "tutorial/035_pUnitType"
Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level-polymorphic unit type
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000412s, checked in 0.000030s
Test "tutorial/036_eqType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Equality, as an important indexed non-recursive data type
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.5 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000485s, checked in 0.000056s
Test "tutorial/037_natDef"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive inductive data type
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.5 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000461s, checked in 0.000035s
Test "tutorial/038_rbTreeDef"
Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive indexed data type
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 14.3 M · max rss memory: 6.9 MB
stderr:
parsed in 0.000885s, checked in 0.000082s
Test "tutorial/039_inductBadNonSort"
Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type with a non-sort type
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
inductive inductBadNonSort : constType
^^^^^^^^^
has type
Type → Type → Type
but is expected to be a Sort (Type or Prop)
parsed in 0.000373s, checked in 0.000085s
Test "tutorial/040_inductBadNonSort2"
Expected: ✋ reject · Size: 602 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Another inductive type with a non-sort type
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
inductive inductBadNonSort2 : aType
^^^^^
has type
Type
but is expected to be a Sort (Type or Prop)
parsed in 0.000431s, checked in 0.000047s
Test "tutorial/041_inductLevelParam"
Expected: ✋ reject · Size: 519 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with duplicate level params
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 6.1 MB
stderr:
Invalid declaration inductLevelParam.{u, u}: duplicate level parameter u
Test "tutorial/042_inductTooFewParams"
Expected: ✋ reject · Size: 552 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with too few parameters in the type
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 10.9 M · max rss memory: 6.0 MB
stderr:
inductive inductTooFewParams : Prop → Prop
^^^^^^^^^^^
has type
Prop
but is expected to be a Sort (Type or Prop)
parsed in 0.000349s, checked in 0.000032s
Test "tutorial/043_inductWrongCtorParams"
Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
inductive inductWrongCtorParams : Prop → Type
| mk : Type → inductWrongCtorParams aProp
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
invalid return type
parsed in 0.000435s, checked in 0.000061s
Test "tutorial/044_inductWrongCtorResParams"
Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters in result (they are swapped)
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
inductive inductWrongCtorResParams : Prop → Prop → Type
| mk : (x : Prop) → (y : Prop) → inductWrongCtorResParams y x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
invalid return type
parsed in 0.000321s, checked in 0.000067s
Test "tutorial/045_inductWrongCtorResLevel"
Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong level parameters in result (they are swapped)
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
inductive inductWrongCtorResLevel.{u1, u2} : Prop → Prop → Type
| mk : (x : Prop) → (y : Prop) → inductWrongCtorResLevel.{u2, u1} x y
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
invalid return type
parsed in 0.000435s, checked in 0.000073s
Test "tutorial/046_inductInIndex"
Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A constructor with an unexpected occurrence of the type in index position of a return type.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
inductive inductInIndex : Prop → Prop
| mk : inductInIndex (inductInIndex aProp)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
invalid return type
parsed in 0.000388s, checked in 0.000059s
Test "tutorial/047_indNeg"
Expected: ✋ reject · Size: 1000 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The classic example of an inductive with negative recursive occurrence
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
inductive indNeg : Type
| mk : (indNeg → indNeg) → indNeg
^^^^^^^^^^^^^^^
arg #1 has a non-positive occurrence of the datatype being declared
parsed in 0.000471s, checked in 0.000068s
Test "tutorial/048_reduceCtorParam.mk"
Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.7 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000625s, checked in 0.000071s
Test "tutorial/049_reduceCtorType.mk"
Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to not reduce the type of the constructor itself;
that should be all manifest foralls
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
inductive reduceCtorType : Type
| mk : id reduceCtorType
^^^^^^^^^^^^^^^^^
invalid return type
parsed in 0.000429s, checked in 0.000084s
Test "tutorial/050_indNegReducible"
Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
inductive indNegReducible : Type
| mk : (constType aType indNegReducible → indNegReducible) → indNegReducible
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
arg #1 has a non-positive occurrence of the datatype being declared
parsed in 0.000501s, checked in 0.000095s
Test "tutorial/051_predWithTypeField"
Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive proposition can have constructors with fields of arbitrary level.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000441s, checked in 0.000051s
Test "tutorial/052_typeWithTypeField"
Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of level up to that of the inductive.
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.2 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000434s, checked in 0.000029s
Test "tutorial/053_typeWithTypeFieldPoly"
Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of level up to that of the inductive (polymorphic variant).
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.3 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000483s, checked in 0.000030s
Test "tutorial/054_typeWithTooHighTypeField.mk"
Expected: ✋ reject · Size: 947 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of from higher universes.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.0 M · max rss memory: 6.2 MB
stderr:
inductive typeWithTooHighTypeField : Type
| mk : Type → typeWithTooHighTypeField
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
has field of type
Type
at universe level 2, but the inductive is at universe level 1
parsed in 0.000430s, checked in 0.000064s
Test "tutorial/055_emptyRec"
Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.1 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000511s, checked in 0.000058s
Test "tutorial/056_boolRec"
Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.5 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000525s, checked in 0.000082s
Test "tutorial/057_twoBoolRec"
Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.0 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000640s, checked in 0.000103s
Test "tutorial/058_andRec"
Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.9 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000572s, checked in 0.000125s
Test "tutorial/059_prodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.1 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000572s, checked in 0.000155s
Test "tutorial/060_pprodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.1 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000547s, checked in 0.000152s
Test "tutorial/061_punitRec"
Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.4 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000511s, checked in 0.000069s
Test "tutorial/062_eqRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 14 ms · instructions: 12.0 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000565s, checked in 0.000178s
Test "tutorial/063_nRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.7 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000609s, checked in 0.000089s
Test "tutorial/064_rbTreeRef"
Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 16.8 M · max rss memory: 7.9 MB
stderr:
parsed in 0.001093s, checked in 0.000675s
Test "tutorial/065_boolPropRec"
Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have more than one constructor.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.3 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000551s, checked in 0.000075s
Test "tutorial/066_existsRec"
Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have one constructors and it carries data.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.0 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000610s, checked in 0.000199s
Test "tutorial/067_sortElimPropRec"
Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.5 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000732s, checked in 0.000164s
Test "tutorial/068_sortElimProp2Rec"
Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index. However, it must occur directly in the result type, with no intervening reduction.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.7 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000615s, checked in 0.000165s
Test "tutorial/069_boolRecEqns"
Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Bool.rec
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.5 M · max rss memory: 6.8 MB
stderr:
parsed in 0.000749s, checked in 0.000149s
Test "tutorial/070_prodRecEqns"
Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Prod.rec
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 14.0 M · max rss memory: 7.0 MB
stderr:
parsed in 0.000715s, checked in 0.000308s
Test "tutorial/071_nRecReduction"
Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A proof relying on the reduction behavior of N.rec
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 14.4 M · max rss memory: 7.0 MB
stderr:
parsed in 0.000814s, checked in 0.000249s
Test "tutorial/072_listRecReduction"
Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of List.rec
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 17.4 M · max rss memory: 8.0 MB
stderr:
parsed in 0.001028s, checked in 0.000790s
Test "tutorial/073_RBTree.id_spec"
Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RBTree.rec
Test result: 👍 accepted · exit code 0 · wall time: 13 ms · instructions: 28.7 M · max rss memory: 11.9 MB
stderr:
parsed in 0.002080s, checked in 0.004053s
Test "tutorial/074_And.right"
Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking simple projection functions
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.9 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000469s, checked in 0.000096s
Test "tutorial/075_Prod.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions with parameters
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.0 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000529s, checked in 0.000128s
Test "tutorial/076_PProd.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.0 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000500s, checked in 0.000117s
Test "tutorial/077_PSigma.snd"
Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking dependent projection functions
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000507s, checked in 0.000158s
Test "tutorial/078_projOutOfRange"
Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Out of range projection
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.7 M · max rss memory: 6.4 MB
stderr:
projOutOfRange : ∀ (x : Prop), ∀ (x : Prop), And x x → x invalid projection And.2: And has only 2 fields parsed in 0.000479s, checked in 0.000080s
Test "tutorial/079_projNotStruct"
Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection out something that is not a structure
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.5 M · max rss memory: 6.4 MB
stderr:
projNotStruct : N → N N is not a structure: it has 2 constructors parsed in 0.000461s, checked in 0.000052s
Test "tutorial/080_projProp1"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000589s, checked in 0.000064s
Test "tutorial/081_projProp2"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
projProp2 : PropStructure.{0, 1} → PUnit.{1}
invalid projection PropStructure.1: cannot project a non-propositional field from a propositional structure
parsed in 0.000593s, checked in 0.000082s
Test "tutorial/082_projProp3"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields. Non-dependent data fields are not relevant.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000604s, checked in 0.000067s
Test "tutorial/083_projProp4"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
projProp4 : PropStructure.{0, 1} → PUnit.{1}
invalid projection PropStructure.3: cannot project a non-propositional field from a propositional structure
parsed in 0.000679s, checked in 0.000087s
Test "tutorial/084_projProp5"
Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows proof projections out of propositional structures that depend on data.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.8 M · max rss memory: 6.6 MB
stderr:
projProp5 : ∀ (x : PropStructure.{0, 1}), Eq x.someMoreData x.someMoreData
invalid projection PropStructure.4: cannot project a non-propositional field from a propositional structure
parsed in 0.000617s, checked in 0.000093s
Test "tutorial/085_projProp6"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition.
The lean kernel rejects any projections out of a proposition that come after a dependent data field, even if that is not used by the present projection.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.5 MB
stderr:
projProp6 : PropStructure.{0, 1} → PUnit.{0}
invalid projection PropStructure.5: cannot project a non-propositional field from a propositional structure
parsed in 0.000633s, checked in 0.000076s
Test "tutorial/086_projDataIndexRec"
Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The recursor for ProjDataIndex allows elimination into sort.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.4 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000580s, checked in 0.000106s
Test "tutorial/087_projIndexData"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.2 M · max rss memory: 6.5 MB
stderr:
projIndexData : (x : N) → ProjDataIndex x → N unknown structure: PropStructure parsed in 0.000606s, checked in 0.000071s
Test "tutorial/088_projIndexData2"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
This also forbids projecting out proofs that follow such fields.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
projIndexData2 : ∀ (x : N), ProjDataIndex x → True unknown structure: PropStructure parsed in 0.000608s, checked in 0.000072s
Test "tutorial/089_projRed"
Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection reductions
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.3 M · max rss memory: 6.8 MB
stderr:
parsed in 0.000686s, checked in 0.000167s
Test "tutorial/090_ruleK"
Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq:
The recursor reduces even if the major argument is not a constructor,
as long replacing the major argument with a constructor is type correct.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.5 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000591s, checked in 0.000121s
Test "tutorial/091_ruleKbad"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq should not fire if the types of the major argument
do not match that of the constructor.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.8 M · max rss memory: 6.6 MB
stderr:
theorem ruleKbad : ∀ (h : Eq Bool.true Bool.false), ∀ (a : Bool), Eq (Eq.rec a h) a := fun x a ↦ Eq.refl a
^^^^^^^^^^^^^^^^^^^
has type
Eq Bool.true Bool.false → ∀ (a : Bool), Eq a a
but is expected to have type
∀ (h : Eq Bool.true Bool.false), ∀ (a : Bool), Eq (Eq.rec a h) a
parsed in 0.000565s, checked in 0.000234s
Test "tutorial/092_ruleKAcc"
Expected: ✋ reject · Size: 12.8 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k should not fire for Acc.
Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 15.0 M · max rss memory: 7.4 MB
stderr:
theorem ruleKAcc.{u} : ∀ (α : Sort u), ∀ (p : ∀ (a : α), ∀ (a : α), Prop), ∀ (x : α), ∀ (h : Acc p x), ∀ (a : Bool), Eq (Acc.rec (fun x x x ↦ a) h) a := fun α p x h a ↦ Eq.refl a
^^^^^^^^^^^^^^^^^^^^^^^^^
has type
∀ (α : Sort u), ∀ (p : ∀ (a : α), ∀ (a : α), Prop), ∀ (x : α), Acc p x → ∀ (a : Bool), Eq a a
but is expected to have type
∀ (α : Sort u), ∀ (p : ∀ (a : α), ∀ (a : α), Prop), ∀ (x : α), ∀ (h : Acc p x), ∀ (a : Bool), Eq (Acc.rec (fun x x x ↦ a) h) a
parsed in 0.000827s, checked in 0.000486s
Test "tutorial/093_aNatLit"
Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.4 M · max rss memory: 6.2 MB
stderr:
parsed in 0.000469s, checked in 0.000032s
Test "tutorial/094_natLitEq"
Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000585s, checked in 0.000075s
Test "tutorial/095_proofIrrelevance"
Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Proof irrelevance
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.1 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000570s, checked in 0.000105s
Test "tutorial/096_unitEta1"
Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.4 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000601s, checked in 0.000106s
Test "tutorial/097_unitEta2"
Expected: 👍 accept · Size: 6.0 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000548s, checked in 0.000100s
Test "tutorial/098_unitEta3"
Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000548s, checked in 0.000099s
Test "tutorial/099_structEta"
Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Structure eta
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 14.6 M · max rss memory: 7.1 MB
stderr:
parsed in 0.000825s, checked in 0.000322s
Test "tutorial/100_funEta"
Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for non-dependent functions.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000603s, checked in 0.000130s
Test "tutorial/101_funEtaDep"
Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for dependent functions (pi types).
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000560s, checked in 0.000141s
Test "tutorial/102_funEtaBad"
Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Eta should not identify functions with different bodies.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.5 M · max rss memory: 6.6 MB
stderr:
theorem funEtaBad : ∀ (α : Type), ∀ (β : Type), ∀ (g : α → α), ∀ (f : α → β), Eq (fun x ↦ f (g x)) f := fun x x x f ↦ Eq.refl f
^^^^^^^^^^^^^^^^^^^^^^^
has type
∀ (x : Type), ∀ (x : Type), ∀ (x : x → x), ∀ (f : x → x), Eq f f
but is expected to have type
∀ (α : Type), ∀ (β : Type), ∀ (g : α → α), ∀ (f : α → β), Eq (fun x ↦ f (g x)) f
parsed in 0.000581s, checked in 0.000244s
Test "tutorial/103_etaRuleK"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied recursor with rule k and a free variable trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 12.7 M · max rss memory: 6.6 MB
stderr:
def etaRuleK : ∀ (a : Eq Bool.true Bool.true → Bool), Eq (Eq.rec (a (Eq.refl Bool.true))) a :=
fun a ↦ Eq.refl a
^^^^^^^^^^^^^^^^^
has type
∀ (a : Eq Bool.true Bool.true → Bool), Eq a a
but is expected to have type
∀ (a : Eq Bool.true Bool.true → Bool), Eq (Eq.rec (a (Eq.refl Bool.true))) a
parsed in 0.000579s, checked in 0.000206s
Test "tutorial/104_etaCtor"
Expected: ✋ reject · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied constructor trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 13.0 M · max rss memory: 6.6 MB
stderr:
def etaCtor : ∀ (x : True → T), Eq (T.mk (T.val (x True.intro))) x :=
fun x ↦ Eq.refl x
^^^^^^^^^^^^^^^^^
has type
∀ (x : True → T), Eq x x
but is expected to have type
∀ (x : True → T), Eq (T.mk (T.val (x True.intro))) x
parsed in 0.000676s, checked in 0.000153s
Test "tutorial/105_reflOccLeft"
Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence on the left of an arrow, behind further arrows inside a constructor argument.
The constructor argument is a function type Nat → (I → Nat).
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 11.6 M · max rss memory: 6.4 MB
stderr:
inductive reflOccLeft : Type
| mk : (Nat → reflOccLeft → Nat) → reflOccLeft
^^^^^^^^^^^^^^^^^^^^^^^
arg #1 has a non-positive occurrence of the datatype being declared
parsed in 0.000450s, checked in 0.000067s
Test "tutorial/106_reflOccInIndex"
Expected: ✋ reject · Size: 4.0 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence in index position, behind a further arrow.
We build an indexed inductive I : Type → Type with a constructor argument
Nat → I (I α), so the recursive occurrence appears as an index argument.
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 11.7 M · max rss memory: 6.4 MB
stderr:
inductive reflOccInIndex : Type → Type
| mk : (α : Type) → ((x : Nat) → reflOccInIndex (reflOccInIndex x)) → reflOccInIndex α
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
has field of type
Type
at universe level 2, but the inductive is at universe level 1
parsed in 0.000430s, checked in 0.000073s
Test "tutorial/107_reduceCtorParamRefl.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 11.9 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000491s, checked in 0.000063s
Test "tutorial/108_reduceCtorParamRefl2.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 11.8 M · max rss memory: 6.4 MB
stderr:
parsed in 0.000522s, checked in 0.000068s
Test "tutorial/109_rTreeRec"
Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.2 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000533s, checked in 0.000096s
Test "tutorial/110_rtreeRecReduction"
Expected: 👍 accept · Size: 10.8 KB · Lines: 193 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RTree.rec on RTree.mk.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.6 M · max rss memory: 6.9 MB
stderr:
parsed in 0.000759s, checked in 0.000199s
Test "tutorial/111_accRecType"
Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Acc.rec.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 13.7 M · max rss memory: 7.0 MB
stderr:
parsed in 0.000626s, checked in 0.000357s
Test "tutorial/112_accRecReduction"
Expected: 👍 accept · Size: 13.4 KB · Lines: 252 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec reduces on Acc.intro.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 15.0 M · max rss memory: 7.2 MB
stderr:
parsed in 0.000831s, checked in 0.000388s
Test "tutorial/113_accRecNoEta"
Expected: ✋ reject · Size: 13.0 KB · Lines: 244 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec does not have structure eta.
Test result: ✋ rejected · exit code 1 · wall time: 8 ms · instructions: 15.0 M · max rss memory: 7.4 MB
stderr:
theorem accRecNoEta : ∀ {α : Type}, ∀ (r : ∀ (a : α), ∀ (a : α), Prop), ∀ (a : α), ∀ (h : Acc r a), ∀ (p : Bool), Eq (Acc.rec (fun x x x ↦ p) h) p := fun α r a h p ↦ Eq.refl p
^^^^^^^^^^^^^^^^^^^^^^^^^
has type
∀ (α : Type), ∀ (r : ∀ (a : α), ∀ (a : α), Prop), ∀ (a : α), Acc r a → ∀ (p : Bool), Eq p p
but is expected to have type
∀ {α : Type}, ∀ (r : ∀ (a : α), ∀ (a : α), Prop), ∀ (a : α), ∀ (h : Acc r a), ∀ (p : Bool), Eq (Acc.rec (fun x x x ↦ p) h) p
parsed in 0.000834s, checked in 0.000476s
Test "tutorial/114_quotMkType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.3 M · max rss memory: 6.5 MB
stderr:
parsed in 0.000559s, checked in 0.000087s
Test "tutorial/115_quotIndType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.ind.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.6 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000590s, checked in 0.000168s
Test "tutorial/116_quotLiftType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.lift.
Test result: 👍 accepted · exit code 0 · wall time: 7 ms · instructions: 12.8 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000598s, checked in 0.000173s
Test "tutorial/117_quotSoundType"
Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.sound.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 12.9 M · max rss memory: 6.6 MB
stderr:
parsed in 0.000642s, checked in 0.000157s
Test "tutorial/118_quotLiftReduction"
Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.lift on Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 13.3 M · max rss memory: 6.9 MB
stderr:
parsed in 0.000795s, checked in 0.000243s
Test "tutorial/119_quotIndReduction"
Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.ind on Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 8 ms · instructions: 13.3 M · max rss memory: 6.9 MB
stderr:
parsed in 0.000721s, checked in 0.000276s
Test "tutorial/120_dup_defs"
Expected: ✋ reject · Size: 479 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Two definitions with the same name
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 6.0 MB
stderr:
Invalid declaration dup_defs: already declared as def dup_defs : Type := Prop
Test "tutorial/121_dup_ind_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 5.9 MB
stderr:
expected name index 4, got 8
Test "tutorial/122_dup_ctor_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 5.9 MB
stderr:
expected name index 4, got 8
Test "tutorial/123_dup_rec_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 6 ms · instructions: 10.8 M · max rss memory: 5.9 MB
stderr:
expected name index 4, got 8
Test "tutorial/124_dup_rec_def2"
Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition with the name of a recursor, and the recursor named differently. This would pass simple checks for duplicate definitions in the parser, but should still be rejected by the checker.
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.8 M · max rss memory: 5.9 MB
stderr:
expected name index 5, got 9
Test "tutorial/125_dup_ctor_rec"
Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A constructor and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 16 ms · instructions: 10.7 M · max rss memory: 5.9 MB
stderr:
expected name index 3, got 6
Test "tutorial/126_DupConCon"
Expected: ✋ reject · Size: 2.2 KB · Lines: 35 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with two constructors with the same name
Test result: ✋ rejected · exit code 1 · wall time: 7 ms · instructions: 10.7 M · max rss memory: 5.9 MB
stderr:
expected name index 4, got 7