587540f11b
This command is not just a cosmetic feature. We need it to defined `id_rhs` before the tactic framework is defined. We want `id_rhs` to be used in all definitions generated by the equation compiler. Right now, it is only used in definitions defined after the tactic framework.
31 lines
1.3 KiB
Text
31 lines
1.3 KiB
Text
?m_1
|
||
nat.succ
|
||
((⟨nat.rec
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)),
|
||
id_rhs ℕ (nat.succ ((_F.fst).fst a)))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
0
|
||
punit.star,
|
||
punit.star⟩
|
||
(λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
|
||
⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
|
||
(λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
|
||
nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
|
||
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)),
|
||
id_rhs ℕ (nat.succ ((_F.fst).fst a)))
|
||
_F)
|
||
a_1
|
||
a
|
||
_F)
|
||
(nat.succ n)
|
||
⟨ih, punit.star⟩,
|
||
⟨ih, punit.star⟩⟩)
|
||
0,
|
||
punit.star⟩.fst).fst
|
||
1)
|