log

age author description
2019-08-11 Shinji KONO ...
2019-08-11 Shinji KONO try transfinite
2019-08-11 Shinji KONO ...
2019-08-11 Shinji KONO set theortic function definition using sup
2019-08-10 Shinji KONO does not work
2019-08-10 Shinji KONO recover ε-induction
2019-08-09 Shinji KONO sepration of ordinal from OD
2019-08-09 Shinji KONO TransFinite induction fixed
2019-08-08 Shinji KONO fix Ordinals
2019-08-07 Shinji KONO try to separate Ordinals
2019-08-07 Shinji KONO separate cardinal
2019-08-06 Shinji KONO try func
2019-08-05 Shinji KONO cardinal continue
2019-08-04 Shinji KONO Cardinal start
2019-08-02 Shinji KONO Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision
2019-08-02 Shinji KONO both
2019-08-02 Shinji KONO separate logic and nat
2019-08-01 Shinji KONO Added tag current for changeset 2c7d45734e3b
2019-08-01 Shinji KONO Axiom of choice from exclude middle release
2019-08-01 Shinji KONO axiom of choice from exclusive middle done
2019-08-01 Shinji KONO ∀-imply-or
2019-07-31 Shinji KONO ...
2019-07-31 Shinji KONO try again ..
2019-07-31 Shinji KONO ...
2019-07-31 Shinji KONO ...
2019-07-31 Shinji KONO Transfinite induction fixed
2019-07-31 Shinji KONO fixing transfinte induction...
2019-07-30 Shinji KONO ε-induction like loop again
2019-07-29 Shinji KONO ...
2019-07-29 Shinji KONO ε-induction again
2019-07-29 Shinji KONO curry form
2019-07-29 Shinji KONO another approach
2019-07-29 Shinji KONO transfinite
2019-07-29 Shinji KONO ...
2019-07-29 Shinji KONO ...
2019-07-29 Shinji KONO emulate ε-induction proof
2019-07-28 Shinji KONO ...
2019-07-28 Shinji KONO does not work
2019-07-28 Shinji KONO choice function cannot jump between ordinal level
2019-07-26 Shinji KONO add filter
2019-07-25 Shinji KONO Axiom of choies implies p ∨ ( ¬ p )
2019-07-25 Shinji KONO axiom of choice → p ∨ ¬ p
2019-07-23 Shinji KONO add Todo
2019-07-22 Shinji KONO fix extensionality
2019-07-22 Shinji KONO ...
2019-07-22 Shinji KONO ...
2019-07-21 Shinji KONO fix zf
2019-07-21 Shinji KONO remove ordinal-definable
2019-07-21 Shinji KONO ...
2019-07-20 Shinji KONO new ordinal-definable
2019-07-19 Shinji KONO fix comments
2019-07-19 Shinji KONO ε-induction release
2019-07-19 Shinji KONO Added tag current for changeset ecb329ba38ac
2019-07-19 Shinji KONO ε-induction done
2019-07-19 Shinji KONO ...
2019-07-19 Shinji KONO ...
2019-07-19 Shinji KONO ...
2019-07-19 Shinji KONO non terminateing on ε-induction
2019-07-18 Shinji KONO ...
2019-07-18 Shinji KONO ...