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 |
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 |