Mercurial > hg > Members > kono > Proof > ZF-in-agda
log
age | author | description |
---|---|---|
Tue, 06 Aug 2019 15:50:14 +0900 | Shinji KONO | try func |
Mon, 05 Aug 2019 17:02:37 +0900 | Shinji KONO | cardinal continue |
Sun, 04 Aug 2019 18:09:00 +0900 | Shinji KONO | Cardinal start |
Fri, 02 Aug 2019 21:31:45 +0900 | Shinji KONO | Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision |
Fri, 02 Aug 2019 16:27:53 +0900 | Shinji KONO | both |
Fri, 02 Aug 2019 12:17:10 +0900 | Shinji KONO | separate logic and nat |