1. Ambrus Kaposi Avatar Ambrus Kaposi
  2. Untitled project
  3. tt-in-tt
  4. Issues

Add new types to the syntax

Issue #1 new
Ambrus Kaposi repo owner created an issue
  • 0,1,2 (in the universe as well)
  • W types
  • M types
  • finish Id
  • inductive inductive types
  • quotient types
  • a hierarchy of universes

Comments (1)

  2. Log in to comment
Assignee
–
Type
enhancement
Priority
major
Status
new
Votes
0
Watchers
1
Jira Software: the preferred issue tracker for Bitbucket. Join the team!