Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff src/OrdUtil.agda @ 796:171123c92007

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Aug 2022 17:57:41 +0900
parents a08c456d49d0
children d70f3f0681ea
line wrap: on
line diff
--- a/src/OrdUtil.agda	Fri Aug 05 16:21:46 2022 +0900
+++ b/src/OrdUtil.agda	Fri Aug 05 17:57:41 2022 +0900
@@ -57,7 +57,7 @@
 ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x                                        
 ob<x {b} {x} lim b<x with trio< (osuc b) x                                                                                     
 ... | tri< a ¬b ¬c = a                                                                                                         
-... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x }  )                                                     
+... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { oprev = b ; oprev=x = ob=x }  )                                                     
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )                           
 
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox