16 lines
402 B
Text
16 lines
402 B
Text
import data.finset
|
|
check @and.rec
|
|
|
|
definition and.rec2 [recursor 4] {p r : Prop} (H₁ : p → r) (H₂ : p ∧ p) : r :=
|
|
and.rec_on H₂ (λ h₁ h₁, H₁ h₁)
|
|
|
|
set_option pp.all true
|
|
check ∃ x : nat, x = x
|
|
|
|
print [recursor] and.rec2
|
|
print [recursor] or.rec
|
|
print [recursor] and.rec
|
|
print [recursor] nat.rec
|
|
print [recursor] finset.induction
|
|
print [recursor] list.rec
|
|
print [recursor] Exists.rec
|