Mercurial > hg > Members > kono > Proof > ZF-in-agda
log
age | author | description |
---|---|---|
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 |
Thu, 01 Aug 2019 15:38:08 +0900 | Shinji KONO | Added tag current for changeset 2c7d45734e3b |