comparison logic.agda @ 215:f15eaa7c5932

Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2019 21:31:45 +0900
parents 22d435172d1a
children 8b0715e28b33
comparison
equal deleted inserted replaced
214:e05575588191 215:f15eaa7c5932