jonsterling/JonPRL

Issues

• Broken links

  #254 opened 5 years ago by arthuraa
  2

• A Module System?

  #252 opened 9 years ago by markfarrell
  0

• Try JonPRL

  #247 opened 9 years ago by markfarrell
  5

• Formalization of Cubical Type Theory

  #251 opened 9 years ago by markfarrell
  2

• Types are ∞-groupoids

  #248 opened 9 years ago by markfarrell
  2

• Internally prove whether or not "axiom K" can be derived?

  #249 opened 9 years ago by markfarrell
  2

• Add universe hierarchy

  #250 opened 9 years ago by jonsterling
  1

• pattern compilation is broken for multiple bindings

  #214 opened 9 years ago by jonsterling
  17

• Integrate delta equalities into computation system

  #183 opened 9 years ago by vrahli
  21

• consider switching to "dependent LCF" refiner

  #245 opened 9 years ago by jonsterling
  2

• higher-order judgments

  #215 opened 9 years ago by jonsterling
  1

• switch per operator signature to (2)

  #241 opened 9 years ago by jonsterling
  2

• Respect for Functionality

  #243 opened 9 years ago by jozefg
  7

• Consider switching to typed ABTs

  #242 opened 9 years ago by jonsterling
  5

• Standard eq-eq rule is not invertible

  #237 opened 9 years ago by jonsterling
  1

• `auto` tactic can crash

  #238 opened 9 years ago by peterohanley
  3

• Better error messages

  #239 opened 9 years ago by jonsterling
  0

• [idea] implement neel's linear type system

  #195 opened 9 years ago by jonsterling
  2

• quotients and PER types

  #213 opened 9 years ago by jonsterling
  7

• Comments

  #186 opened 9 years ago by vrahli
  2

• DecideEq is broken

  #233 opened 9 years ago by jozefg
  2

• Begin tagging versions / releases

  #232 opened 9 years ago by jonsterling
  1

• Document containers, trees, extensions, neighborhoods, etc.

  #231 opened 9 years ago by jonsterling
  0

• Importing libraries

  #226 opened 9 years ago by vrahli
  5

• Configuration files don't support "/"

  #229 opened 9 years ago by jonsterling
  1

• Canonical-forms tests

  #222 opened 9 years ago by jonsterling
  0

• improvements to container theory

  #220 opened 9 years ago by jonsterling
  0

• Make JonPRL SML '97 Compatible

  #218 opened 9 years ago by jozefg
  7

• Are the Image rules sound? [Question]

  #219 opened 9 years ago by jonsterling
  2

• "late binding" for resource tactic

  #216 opened 9 years ago by jonsterling
  0

• User Defined Resources

  #209 opened 9 years ago by jozefg
  1

• Targeted Reduce and Unfold

  #208 opened 9 years ago by jozefg
  1

• expose PROGRESS tactical

  #200 opened 9 years ago by jonsterling
  0

• Add exceptions to computation system

  #194 opened 9 years ago by jonsterling
  0

• Nuprl-style equality type

  #161 opened 9 years ago by jonsterling
  4

• elim rule for approx

  #190 opened 9 years ago by jonsterling
  2

• No admit tactic

  #179 opened 9 years ago by wilcoxjay
  0

• Witness accepts terms with free variables

  #181 opened 9 years ago by vrahli
  2

• Unfold does not unfold all occurrences

  #177 opened 9 years ago by wilcoxjay
  2

• Semicolon parsed inconsistently

  #178 opened 9 years ago by wilcoxjay
  0

• tactic arguments

  #169 opened 9 years ago by jonsterling
  1

• rudimentary build system for developments (à la Twelf)

  #150 opened 9 years ago by jonsterling
  1

• The tactic "fail" fails to parse

  #173 opened 9 years ago by wilcoxjay
  2

• Problem using Eval with sums

  #170 opened 9 years ago
  1

• get rid of CUSTOM operator?

  #165 opened 9 years ago by jonsterling
  4

• Print, Compute, and Search

  #155 opened 9 years ago by vrahli
  3

• use sml-open-abt

  #162 opened 9 years ago by jonsterling
  0

• Implement squash-intro tactic

  #149 opened 9 years ago by jonsterling
  0

• computational effects

  #148 opened 9 years ago by jonsterling
  0

• How do the universe levels work?

  #146 opened 9 years ago
  4