Issues

• Factor out Favonia Namespace code into library

  RedPRL/redtt#488 · Filter by author jonsterling opened on Jan 10, 2020
  3

  

• Currying inside systems

  RedPRL/redtt#480 · Filter by author 3abc opened on Feb 13, 2019
  1

• Mortality

  bug
  RedPRL/redtt#477 · Filter by author kaonn opened on Jan 15, 2019
  6

  

• Decompose elim into rec and case

  Thought
  RedPRL/redtt#454 · Filter by author jonsterling opened on Oct 28, 2018
  2

• Private data types

  RedPRL/redtt#409 · Filter by author favonia opened on Oct 17, 2018

• Implement the cleanliness checking.

  RedPRL/redtt#408 · Filter by author favonia opened on Oct 17, 2018

• Resolution of constructor names

  RedPRL/redtt#402 · Filter by author favonia opened on Oct 16, 2018
  2

• Concrete notation of coe sucks!

  RedPRL/redtt#400 · Filter by author jonsterling opened on Oct 16, 2018
  3

• Weird bug when trying to introduce pi type

  RedPRL/redtt#377 · Filter by author jonsterling opened on Oct 10, 2018

• Current coe of fhcom type is wrong

  RedPRL/redtt#367 · Filter by author favonia opened on Oct 5, 2018

• Strict Propositions

  RedPRL/redtt#357 · Filter by author spitters opened on Sep 24, 2018
  1

• Expose generalize tactic to the user

  RedPRL/redtt#333 · Filter by author jonsterling opened on Sep 17, 2018
  2

• Unify all the code that checks composition-like operators

  RedPRL/redtt#332 · Filter by author jonsterling opened on Sep 17, 2018

• Tactic to hide hypotheses

  RedPRL/redtt#326 · Filter by author jonsterling opened on Sep 17, 2018

• projecting from opaque pair

  bug
  RedPRL/redtt#313 · Filter by author ecavallo opened on Sep 12, 2018

• Idea: let Quote control unfolding

  RedPRL/redtt#268 · Filter by author jonsterling opened on Aug 29, 2018
  4

• Combinatorial explosion

  RedPRL/redtt#259 · Filter by author guillaumebrunerie opened on Aug 21, 2018
  4

• Eta-expand constructors immediately

  RedPRL/redtt#257 · Filter by author favonia opened on Aug 21, 2018
  8

• Thought about agda-style top-level definitions

  Thought
  RedPRL/redtt#251 · Filter by author jonsterling opened on Aug 18, 2018
  3

• Find a way to implement strict composition

  RedPRL/redtt#238 · Filter by author ecavallo opened on Aug 16, 2018
  5

• Log levels for output hygiene

  frontend
  RedPRL/redtt#225 · Filter by author jonsterling opened on Aug 13, 2018
  1

• non-dependent recursors for HITs

  enhancementevaluator
  RedPRL/redtt#214 · Filter by author ecavallo opened on Aug 9, 2018
  7

• Consider implementing com on a connective-by-connective basis

  evaluator
  RedPRL/redtt#213 · Filter by author jonsterling opened on Aug 9, 2018
  1

• Non-trivial argument types in CITs

  elaboratorenhancementevaluatorparsertypechecker
  RedPRL/redtt#202 · Filter by author jonsterling opened on Aug 6, 2018
  6

• Indexed cubical inductive types

  elaboratorenhancementevaluatorparsertypechecker
  RedPRL/redtt#201 · Filter by author jonsterling opened on Aug 6, 2018