🚧 🦆 Inductive Types - #295

Draft

TOTBWF wants to merge 5 commits into

mainfrom

theory-of-inductives

Commits on Jan 13, 2022

[WIP] Define the internal theory of inductive types
TOTBWF
committed
671bb03

Commits on Jan 14, 2022

[WIP] Add codes for desc, ctx, and tm
TOTBWF
committed
a835be9

Commits on Jan 18, 2022

[WIP] Computing elimination methods
TOTBWF
committed
e015e6a
Add unit tests for inductive types
TOTBWF
committed
7e8a3a2

Commits on Jan 19, 2022

[WIP] Rework 'DescMethod', start adding in 'Elem' machinery
TOTBWF
committed
32f9e4c