RedPRL/sml-redprl

Issues

• link to picture in README.md is invalid

  #703 opened 2 years ago by mb6ockatf
  1

• Warning about too many tactics in `[_, _, ..., _]`

  #592 opened 2 years ago by favonia
  4

• Sync .mlb and .cm

  #655 opened 2 years ago by favonia
  0

• Rewrite in reverse

  #609 opened 2 years ago by favonia
  0

• Auto tactic should peek into the equations in coe/hcom instead trying all rules in sequence

  #639 opened 2 years ago by favonia
  0

• "Compile SML raised: Option" on initial build

  #696 opened 6 years ago by shingarov
  4

• Recursor for parametric type seems broken

  #694 opened 6 years ago by konn
  2

• Coe of V is wrong

  #692 opened 6 years ago by favonia
  0

• Set up CONTRIBUTING and solve (most) legal issues at once

  #626 opened 7 years ago by favonia
  1

• Add typed beta rules for (vproj x (vin x...)) etc.

  #683 opened 7 years ago by jonsterling
  2

• {foo,bar} should match either (1) tuples with proj1 and proj2 or more, or (2) tuples with foo and bar and more, but definitely nothing else!

  #584 opened 7 years ago by favonia
  5

• Better freshing/renaming?

  #640 opened 7 years ago by favonia
  5

• don’t require uppercase operator names

  #651 opened 7 years ago by jonsterling
  8

• Fix automation

  #569 opened 7 years ago by jonsterling
  2

• Pretty printer should avoid accidental capturing

  #591 opened 7 years ago by favonia
  4

• Vim mode: show RedPRL is running

  #589 opened 7 years ago by favonia
  4

• Zipper/view for neutral terms

  #583 opened 7 years ago by favonia
  0

• Same flexibility in synth of ($ f x) as of (@ p r).

  #613 opened 7 years ago by favonia
  6

• Add exceptions

  #619 opened 7 years ago by favonia
  4

• Eta and EqCap of fcom types

  #634 opened 7 years ago by favonia
  0

• Eta for V types

  #635 opened 7 years ago by favonia
  0

• Correctly highlight accessors (left, right, type)

  #575 opened 7 years ago by favonia
  16

• Typed binders for theorems and definitions?

  #659 opened 7 years ago by favonia
  0

• Inductive types in multiverses

  #670 opened 7 years ago by favonia
  0

• Better handling of stuck terms?

  #675 opened 7 years ago by favonia
  0

• Handling of meta variables in Restriction.restrict

  #680 opened 7 years ago by favonia
  1

• Bug in the logic of Restriction.restrict?

  #668 opened 7 years ago by favonia
  3

• Bug in HCom.Eq

  #664 opened 7 years ago by jonsterling
  2

• Remove aliases VV and WU?

  #676 opened 7 years ago by favonia
  0

• Make U^pre and U^hcom Kan again!

  #647 opened 7 years ago by favonia
  3

• Implement the grammars and judgments in Part IV.A

  #574 opened 7 years ago by favonia
  61

• Change the syntax of Thm?

  #645 opened 7 years ago by favonia
  2

• Prove the computation rule for J

  #627 opened 7 years ago by mortberg
  12

• Print integers as (int i).

  #628 opened 7 years ago by favonia
  4

• Make Pygments Immortal

  #622 opened 7 years ago by favonia
  0

• Test documentation building in travis

  #621 opened 7 years ago by favonia
  0

• Write a technical document explaining the mini metalanguage

  #624 opened 7 years ago by jonsterling
  0

• Funding acknowledgements

  #580 opened 7 years ago by favonia
  4

• Remove weak booleans.

  #612 opened 7 years ago by favonia
  1

• Handling of meta variables in branchOnDim

  #605 opened 7 years ago by favonia
  0

• Less terrible dependant rewrite.

  #602 opened 7 years ago by favonia
  0

• synthTerm should return aux goals in a separate list

  #595 opened 7 years ago by favonia
  3

• Print (U 0) instead of (U 0 stable)

  #594 opened 7 years ago by favonia
  4

• Dependent rewriting rule

  #593 opened 7 years ago by favonia
  10

• for PRs, allow only squash or rebase, and demand testing to be passed?

  #587 opened 7 years ago by favonia
  9

• Stop pattern matching from unfolding the types unnecessarily.

  #585 opened 7 years ago by favonia
  1

• Consider adding motives to the terms for `if` and `nat-rec`

  #559 opened 7 years ago by jonsterling
  10

• travis testing succeeds even if some examples are failing

  #578 opened 7 years ago by favonia
  2

• Update README with a new section about Vim

  #572 opened 7 years ago by favonia
  2

• Top-level missing source locations

  #567 opened 7 years ago by cangiuli
  0