lean2/tests/lean/whnf.lean.expected.out at 2bd8f969d545798ff61f4bf01e3a5a578f67c6a4 - michael/lean2 - Forgejo: Beyond coding. We forge.

michael/lean2

Leonardo de Moura 064ecd3e3d refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package

We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.

2014-11-22 00:19:39 -08:00

5 lines

182 B

Text

Raw Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 whnf.lean:2:0: warning: imported file uses 'sorry'
 succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) zero)
 succ (succ (succ zero))
 succ (nat.rec a (λ (b₁ r : ℕ), succ r) zero)
 succ a