Code

🚧 🦆 Inductive Types#295

Code

Draft

TOTBWF wants to merge 5 commits intomainRedPRL/cooltt:mainfrom theory-of-inductivesRedPRL/cooltt:theory-of-inductivesCopy head branch name to clipboard

+1,338-204

Commits

Commits on Jan 13, 2022

• [WIP] Define the internal theory of inductive types

  TOTBWF

  committed
  671bb03

  Copy full SHA for 671bb03

Commits on Jan 14, 2022

• [WIP] Add codes for desc, ctx, and tm

  TOTBWF

  committed
  a835be9

  Copy full SHA for a835be9

Commits on Jan 18, 2022

• [WIP] Computing elimination methods

  TOTBWF

  committed
  e015e6a

  Copy full SHA for e015e6a

• Add unit tests for inductive types

  TOTBWF

  committed
  7e8a3a2

  Copy full SHA for 7e8a3a2

Commits on Jan 19, 2022

• [WIP] Rework 'DescMethod', start adding in 'Elem' machinery

  TOTBWF

  committed
  32f9e4c

  Copy full SHA for 32f9e4c