mlang

• when you are not sure, implement the one that is 1. easy to implement 2. restricted 3. enough for now

• roadmap

  • totally unsafe basics
    • basic syntax and parser
    • eta rule
  • coverage checker
    • overlapping patterns
  • mutual recursive functions
  • user defined eliminations
  • HTML pretty print
  • naming shadowing
  • evaluator control
    • error reporting
  • record calculus
  • recursive types
    • inductive families of two flavor
    • hit
    • inductive-inductive
    • inductive-recursive
  • cubical features
  • termination checking
  • implicit arguments
  • implicit conversions
  • structural editor
    • modules and compile unit
  • universe polymorphism
  • coinductive types

math

• quick sort and properties
• symmetry book
• cubical Agda
• Agda stdlib
• Artin's or Lang's Algebra
• Agda's test cases and it's issues
• https://ncatlab.org/homotopytypetheory/show/open+problems#higher_algebra_and_higher_category_theory
  • seems interesting: limits problem?
• https://github.com/HoTT/HoTT
• unimath
• the big problems list
• Agda Katas

misc

• translate to Agda to do correctness checking