RedPRL/cooltt issues and pull requests

#100 - Interactive normalization/type-checking API

Issue - State: closed - Opened by favonia over 4 years ago - 1 comment

#99 - Some top-level improvements (add print command)

Pull Request - State: closed - Opened by jonsterling over 4 years ago - 4 comments

#98 - Update README.md

Pull Request - State: closed - Opened by favonia over 4 years ago

#97 - Correct typo in README

Pull Request - State: closed - Opened by jonsterling over 4 years ago

#96 - Update README.md

Pull Request - State: closed - Opened by favonia over 4 years ago

#95 - first cut at #65

Pull Request - State: closed - Opened by ivoysey over 4 years ago - 1 comment

#94 - Grammar hacks 3.0

Pull Request - State: closed - Opened by favonia over 4 years ago - 5 comments

#93 - Use sedlex (or any Unicode-friendly lexer)

Issue - State: closed - Opened by favonia over 4 years ago - 3 comments

#92 - Grammar experiments

Pull Request - State: closed - Opened by favonia over 4 years ago - 6 comments

#91 - pathd, more tests, and vim signs

Pull Request - State: closed - Opened by cangiuli over 4 years ago - 5 comments

#90 - fix #89

Pull Request - State: closed - Opened by jonsterling over 4 years ago

#89 - multi-lambdas and el

Issue - State: closed - Opened by cangiuli over 4 years ago - 1 comment

#88 - More frontend polish; vim mode

Pull Request - State: closed - Opened by cangiuli over 4 years ago

#87 - N-ary splits in core syntax and domain.

Pull Request - State: closed - Opened by favonia over 4 years ago - 2 comments

#86 - Silent tacit holes `?_`

Issue - State: closed - Opened by jonsterling over 4 years ago - 1 comment
Labels: papercut

#85 - Refactor cof checking

Pull Request - State: closed - Opened by favonia over 4 years ago - 13 comments

#84 - adding type-in-type for now; fixing nat-elim; remember source names

Pull Request - State: closed - Opened by jonsterling over 4 years ago - 1 comment

#83 - Default to elaborating Kan types

Issue - State: closed - Opened by jonsterling over 4 years ago

#82 - Projecting Thoughts to cofibration checking

Pull Request - State: closed - Opened by favonia over 4 years ago - 2 comments

#81 - serialize core language

Issue - State: closed - Opened by ivoysey over 4 years ago
Labels: enhancement

#80 - Refactor cof checking to Favonia's liking 😜

Issue - State: closed - Opened by favonia over 4 years ago - 5 comments
Labels: discussion, code quality

#79 - El up to isomorphism

Pull Request - State: closed - Opened by jonsterling over 4 years ago

#78 - Simplify test_sequent and left_invert_under_cof.

Pull Request - State: closed - Opened by favonia over 4 years ago - 4 comments

#77 - Cleanup Round 2

Pull Request - State: closed - Opened by jonsterling over 4 years ago

#76 - Remember names of bound variables

Issue - State: closed - Opened by jonsterling over 4 years ago - 1 comment

#75 - N-ary split tactics

Issue - State: closed - Opened by jonsterling over 4 years ago - 1 comment
Labels: enhancement

#74 - remove binary meet and join interfaces

Pull Request - State: closed - Opened by jonsterling over 4 years ago - 1 comment

#73 - Random cleanup

Pull Request - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#72 - Update CONTRIBUTORS and LICENSE

Pull Request - State: closed - Opened by jonsterling almost 5 years ago

#71 - Revert "Grammar hacks (#70)"

Pull Request - State: closed - Opened by jonsterling almost 5 years ago

#70 - Grammar hacks

Pull Request - State: closed - Opened by favonia almost 5 years ago

#69 - Grammar 🧞 in service

Issue - State: closed - Opened by cangiuli almost 5 years ago - 26 comments

#68 - Serialization and imports

Issue - State: open - Opened by cangiuli almost 5 years ago - 3 comments

#67 - restore nat tests

Issue - State: closed - Opened by ivoysey almost 5 years ago

#66 - User-friendly pretty printer

Issue - State: closed - Opened by ivoysey almost 5 years ago - 14 comments
Labels: question

#65 - port over redtt.el

Issue - State: closed - Opened by ivoysey almost 5 years ago - 1 comment

#64 - stack overflow in cmdliner

Issue - State: closed - Opened by ivoysey almost 5 years ago - 2 comments
Labels: bug

#63 - Source locations

Pull Request - State: closed - Opened by jonsterling almost 5 years ago - 6 comments

#62 - deletion fest 2020 per #42

Pull Request - State: closed - Opened by ivoysey almost 5 years ago

#61 - selectively bind arguments in a multi-lambda?

Issue - State: open - Opened by ecavallo almost 5 years ago - 2 comments
Labels: enhancement

#60 - Change nat-elim to take a Kan code as an argument

Issue - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#59 - Fix let

Pull Request - State: closed - Opened by jonsterling almost 5 years ago

#58 - trouble with let

Issue - State: closed - Opened by ecavallo almost 5 years ago - 2 comments

#57 - implement coe for path types

Pull Request - State: closed - Opened by ivoysey almost 5 years ago - 1 comment

#56 - Miscellaneous syntax improvements

Pull Request - State: closed - Opened by cangiuli almost 5 years ago - 7 comments

#55 - try switching the CI over

Pull Request - State: closed - Opened by jonsterling almost 5 years ago

#54 - Let the user define an Open Modality

Issue - State: open - Opened by jonsterling almost 5 years ago - 1 comment

#53 - minor oddities (+ one bug)

Pull Request - State: closed - Opened by ecavallo almost 5 years ago

#52 - when quoting in pi type, bind var inside lam

Pull Request - State: closed - Opened by ecavallo almost 5 years ago

#51 - tidy up printing of hole information

Pull Request - State: closed - Opened by ivoysey almost 5 years ago - 5 comments

#50 - Conversion under complex cofibration

Issue - State: closed - Opened by jonsterling almost 5 years ago
Labels: bug

#49 - Close #44.

Pull Request - State: closed - Opened by favonia almost 5 years ago - 1 comment

#48 - FHCom of Nat, bug fixes

Pull Request - State: closed - Opened by jonsterling almost 5 years ago - 2 comments

#47 - Remove Double Equal Signs.

Pull Request - State: closed - Opened by favonia almost 5 years ago - 3 comments

#46 - maybe factor out some commonly built terms

Issue - State: closed - Opened by ivoysey almost 5 years ago - 1 comment
Labels: code quality

#45 - Add hcom and com to surface language.

Pull Request - State: closed - Opened by cangiuli almost 5 years ago - 2 comments

#44 - Grammar paper-cuts

Issue - State: closed - Opened by jonsterling almost 5 years ago
Labels: enhancement

#43 - add "fhcom" for nat

Issue - State: closed - Opened by jonsterling almost 5 years ago

#42 - Remove identity type (now that we have Path)

Issue - State: closed - Opened by jonsterling almost 5 years ago - 2 comments

#41 - Add "Cone of Silence" tactic

Issue - State: closed - Opened by jonsterling almost 5 years ago

#40 - Add coe to surface language.

Pull Request - State: closed - Opened by cangiuli almost 5 years ago - 1 comment

#39 - Add types for the "fiber of El at A under \phi"

Issue - State: open - Opened by jonsterling almost 5 years ago - 1 comment

#38 - don't print vacuous cofibrations

Issue - State: closed - Opened by ivoysey almost 5 years ago - 16 comments
Labels: enhancement

#37 - Quotation doesn't always bind a cofibration proof properly!

Issue - State: closed - Opened by jonsterling almost 5 years ago
Labels: bug

#36 - Treat binders in hcom/coe as functions rather than closures

Issue - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#35 - Consider moving many of the custom closures to 'con'

Issue - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#34 - Get rid of weird 'gtp' stuff

Issue - State: closed - Opened by jonsterling almost 5 years ago
Labels: good first issue

#33 - Add codes for path types

Pull Request - State: closed - Opened by jonsterling almost 5 years ago - 5 comments

#32 - A flat modality for the LF

Issue - State: closed - Opened by jonsterling almost 5 years ago - 2 comments
Labels: wontfix

#31 - Universe decoding up to (strict) iso

Issue - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#30 - unifying closure types, removing cleverness

Pull Request - State: closed - Opened by jonsterling almost 5 years ago

#29 - starting to implement cubical subtypes (#28)

Pull Request - State: closed - Opened by jonsterling almost 5 years ago - 1 comment

#28 - Cubical subtypes

Issue - State: closed - Opened by jonsterling almost 5 years ago

#27 - Elaboration of partial elements

Issue - State: closed - Opened by jonsterling about 5 years ago

#26 - Elaboration of coe

Issue - State: closed - Opened by jonsterling about 5 years ago

#25 - Elaboration of hcom

Issue - State: closed - Opened by jonsterling about 5 years ago

#24 - Elaboration relative to a boundary

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

#23 - Extension type

Issue - State: closed - Opened by jonsterling about 5 years ago - 4 comments

#22 - Partial element pretypes

Issue - State: closed - Opened by jonsterling about 5 years ago

#21 - Cubical subtypes

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

#20 - Cubical evaluation

Pull Request - State: closed - Opened by jonsterling about 5 years ago

#19 - abstract out concrete identifiers

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

#18 - Setup GitHub Actions

Pull Request - State: closed - Opened by jonsterling about 5 years ago

#17 - Source locations

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

#16 - Binary equate, semi-kovacs-style evaluator

Pull Request - State: closed - Opened by jonsterling about 5 years ago

#15 - Add universe a la Tarski

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

#14 - Add "veils" for opacity

Issue - State: closed - Opened by jonsterling about 5 years ago

#13 - implementing J (probably wrong, insomnia)

Pull Request - State: closed - Opened by jonsterling about 5 years ago

#12 - Move general-purpose code into a local basis library

Issue - State: closed - Opened by jonsterling about 5 years ago

#11 - Replace core typechecker with "replay" elaborator

Issue - State: closed - Opened by jonsterling about 5 years ago

#10 - working on abstracting nbe into custom monads

Pull Request - State: closed - Opened by jonsterling about 5 years ago

#9 - Lightweight unification

Issue - State: open - Opened by jonsterling about 5 years ago

#8 - split global / local env

Issue - State: closed - Opened by jonsterling about 5 years ago

#7 - Use unique identifiers for top-level declarations

Issue - State: closed - Opened by jonsterling about 5 years ago

#6 - Combine check-env with elab-env

Issue - State: closed - Opened by jonsterling about 5 years ago

#5 - Higher Ch'i Pretty Printer

Issue - State: closed - Opened by jonsterling about 5 years ago
Labels: help wanted, good first issue

#4 - Substitution up to isomorphism

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment
Labels: discussion

#3 - Switch to traditional non-stratified "A type" judgment

Issue - State: closed - Opened by jonsterling about 5 years ago

#2 - Add coercions to core language

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment
Labels: blocked

#1 - Add elaborator, top-level language

Issue - State: closed - Opened by jonsterling about 5 years ago - 1 comment

GitHub / RedPRL/cooltt issues and pull requests