7cfac38eda
This also involves: - adding definitions about logic and natural numbers existing in the standard library to init - porting the current algebraic hierarchy
44 lines
719 B
Text
44 lines
719 B
Text
Prop:Type
|
||
theorem:definition
|
||
by simp;by exact sorry
|
||
|
||
true:unit
|
||
trivial:star
|
||
is_true:is_unit
|
||
|
||
false:empty
|
||
is_false:is_empty
|
||
|
||
induction:rec
|
||
induction_on:rec_on
|
||
|
||
∨;⊎
|
||
or.elim:sum.rec_on
|
||
or.inl:sum.inl
|
||
or.inr:sum.inr
|
||
or.intro_left _;sum.inl
|
||
or.intro_right _;sum.inr
|
||
or_resolve_right:sum_resolve_right
|
||
or_resolve_left:sum_resolve_left
|
||
or.swap:sum.swap
|
||
or.rec_on:sum.rec_on
|
||
or_of_or_of_imp_of_imp:sum_of_sum_of_imp_of_imp
|
||
or_of_or_of_imp_left:sum_of_sum_of_imp_left
|
||
or_of_or_of_imp_right:sum_of_sum_of_imp_right
|
||
|
||
∧;×
|
||
and.intro:pair
|
||
and.left:
|
||
and.elim_left:prod.pr1
|
||
and.left:prod.pr1
|
||
and.elim_right:prod.pr2
|
||
and.right:prod.pr2
|
||
|
||
∀;Π
|
||
|
||
∃;Σ
|
||
exists.intro:sigma.mk
|
||
exists.elim:sigma.rec_on
|
||
|
||
eq.symm:inverse
|
||
congr_arg:ap
|