7 lines
145 B
Markdown
7 lines
145 B
Markdown
|
Cumulative hierarchy in Coq
|
||
|
|
---------------------------
|
||
|
|
|
||
|
|
Aczel's model of CZF done in Coq.
|
||
|
|
|
||
|
|
Uses [std++](https://gitlab.mpi-sws.org/iris/stdpp).
|