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

comparison ordinal.agda @ 202:ed88384b5102

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-induction like loop again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jul 2019 17:52:15 +0900
parents 65e1b2e415bb
children 8edd2a13a7f3
comparison
equal deleted inserted replaced
201:a1a7caa8b305 202:ed88384b5102
11 data OrdinalD {n : Level} : (lv : Nat) → Set n where 11 data OrdinalD {n : Level} : (lv : Nat) → Set n where
12 Φ : (lv : Nat) → OrdinalD lv 12 Φ : (lv : Nat) → OrdinalD lv
13 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv 13 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
14 14
15 record Ordinal {n : Level} : Set n where 15 record Ordinal {n : Level} : Set n where
16 constructor ordinal
16 field 17 field
17 lv : Nat 18 lv : Nat
18 ord : OrdinalD {n} lv 19 ord : OrdinalD {n} lv
19 20
20 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where 21 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where