文件名称：Ordinal
文件大小：57KB
文件格式：ZIP
更新时间：2024-04-19 06:29:08
Coq
Coq中的序数 普通人 我们定义序数如下。 Inductive t: Type := | build (A: Type) (os: A -> t) . Inductive le: t -> t -> Prop := | le_intro A0 A1 os0 os1 (LE: forall (a0: A0), exists (a1: A1), le (os0 a0) (os1 a1)) : le (build os0) (build os1) . Variant lt: t -> t -> Prop := | lt_intro o A os (a: A) (LE: le o (os a)) : lt o (build os) . 这个定义在集合论中享有序数的许多特性。
【文件预览】：
Ordinal-main
----opam(463B)
----src()
--------Zorn.v(13KB)
--------Fixedpoint.v(5KB)
--------Inaccessible.v(14KB)
--------Cardinal.v(50KB)
--------WfRel.v(10KB)
--------sflib.v(37KB)
--------ToSet.v(12KB)
--------Inaccessibility.v(22KB)
--------WellOrdering.v(13KB)
--------Arithmetic.v(28KB)
--------ClassicalOrdinal.v(34KB)
--------Ordinal.v(45KB)
--------Totalness.v(2KB)
--------Basics.v(2KB)
----README.md(2KB)
----Makefile(542B)
----.gitignore(144B)