redprl/redtt issues and pull requests

#490 - Make redtt run again

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

#489 - Enable type inference for Menhir.

Pull Request - State: closed - Opened by fpottier about 3 years ago - 1 comment

#488 - Factor out Favonia Namespace code into library

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

#487 - updating versions

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

#486 - Upgrade compiler and dependencies

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

#485 - Is there editor support for .red code?

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

#484 - Use Stdlib instead of Pervasives.

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

#483 - Some code golfing ;)

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

#482 - Parametric smash

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

#481 - Is "path of path compositions" available?

Issue - State: closed - Opened by anqurvanillapy over 5 years ago - 2 comments

#480 - Currying inside systems

Issue - State: open - Opened by 3abc almost 6 years ago - 1 comment

#479 - pullbacks

Pull Request - State: closed - Opened by clayrat about 6 years ago - 1 comment

#478 - add some Isos and helper functions

Pull Request - State: closed - Opened by clayrat about 6 years ago

#477 - Mortality

Issue - State: open - Opened by kaonn about 6 years ago - 6 comments
Labels: bug

#476 - smalltt

Issue - State: closed - Opened by spitters about 6 years ago - 2 comments

#475 - delete commented paths.s1 code

Pull Request - State: closed - Opened by ecavallo about 6 years ago

#474 - successor on biinv-int which cancels pred exactly

Pull Request - State: closed - Opened by ecavallo about 6 years ago - 5 comments

#473 - drastically improve hopf performance

Pull Request - State: closed - Opened by ecavallo about 6 years ago - 1 comment

#472 - make connection/both a little better

Pull Request - State: closed - Opened by ecavallo about 6 years ago

#471 - What is the relationship between redtt and redprl?

Issue - State: closed - Opened by outlace about 6 years ago - 1 comment
Labels: question

#470 - use cap tactic in paths.s2

Pull Request - State: closed - Opened by ecavallo about 6 years ago - 1 comment

#469 - proofs about HIT-style integers

Pull Request - State: closed - Opened by ecavallo about 6 years ago - 1 comment

#468 - Backport changes from the new-domain branch.

Pull Request - State: closed - Opened by favonia about 6 years ago

#467 - Box and cap tactics

Pull Request - State: closed - Opened by favonia about 6 years ago - 1 comment

#466 - define inverse(??) to associator?

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

#465 - Misc lemmas

Pull Request - State: closed - Opened by clayrat about 6 years ago - 2 comments

#464 - some facts about smash product

Pull Request - State: closed - Opened by ecavallo about 6 years ago - 2 comments

#463 - Fix Unicode printing of unresolved variables.

Pull Request - State: closed - Opened by cangiuli about 6 years ago

#462 - [vim] Usability improvements.

Pull Request - State: closed - Opened by cangiuli about 6 years ago - 7 comments

#461 - print mismatched names in Quote

Pull Request - State: closed - Opened by clayrat about 6 years ago

#460 - sphere1-to-s1 equivalence

Pull Request - State: closed - Opened by ecavallo about 6 years ago

#459 - Backport changes from the new domain.

Pull Request - State: closed - Opened by favonia about 6 years ago

#458 - Detect cyclic module dependency.

Pull Request - State: closed - Opened by favonia over 6 years ago - 1 comment
Labels: bug

#457 - WIP Diaconescu's theorem

Pull Request - State: open - Opened by clayrat over 6 years ago - 12 comments

#456 - Unary and binary natural numbers.

Pull Request - State: closed - Opened by cangiuli over 6 years ago - 2 comments

#455 - using Cubical Thought in coe/symm/d

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

#454 - Decompose elim into rec and case

Issue - State: open - Opened by jonsterling over 6 years ago - 2 comments
Labels: Thought

#453 - rename triv to ★, random cleanup

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

#452 - Tm.FortyTwo backported from the new-domain PR

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

#451 - Syntax and semantics of namespaces

Issue - State: closed - Opened by favonia over 6 years ago - 2 comments
Labels: Thought

#450 - [Rot] Phase 5: be ^^cooler^^

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

#449 - Syntax and semantics of name modifiers (v5.1, WIP)

Issue - State: closed - Opened by favonia over 6 years ago - 7 comments
Labels: Thought

#448 - support for Opam 2.0.1

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

#447 - add bool paths, DNE, LEM, aux proofs, refactor

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

#446 - added WIP GCD stuff

Pull Request - State: closed - Opened by kaonn over 6 years ago - 1 comment

#445 - Some changes about ghcom

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

#444 - Backport changes frow the new-domain PR.

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

#443 - Type checking of composite types in NewTyping

Issue - State: closed - Opened by jonsterling over 6 years ago
Labels: wontfix, typechecker

#442 - Typechecking of HITs in NewTyping

Issue - State: closed - Opened by jonsterling over 6 years ago
Labels: wontfix, typechecker

#441 - Systematic error type in NewQuote

Issue - State: closed - Opened by jonsterling over 6 years ago - 1 comment
Labels: help wanted, wontfix, cleanup

#440 - Systematic error type in NewDomain

Issue - State: closed - Opened by jonsterling over 6 years ago
Labels: help wanted, wontfix, cleanup

#439 - rot++

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

#438 - Bring new-domain up to date with master

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

#433 - Update Refiner for new domain

Issue - State: closed - Opened by jonsterling over 6 years ago - 1 comment
Labels: elaborator

#430 - Importer/GlobalEnv/ResEnv rectification campaign

Issue - State: closed - Opened by favonia over 6 years ago

#429 - loosen version bounds, upgrade packages

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

#425 - New typechecker

Issue - State: closed - Opened by jonsterling over 6 years ago
Labels: wontfix, typechecker

#423 - POSIX mount semantics [WIP]

Issue - State: closed - Opened by favonia over 6 years ago - 3 comments
Labels: Thought

#422 - ^cooler^ invariance example

Pull Request - State: closed - Opened by cangiuli over 6 years ago - 2 comments

#421 - rename "spine" to "stack"

Issue - State: closed - Opened by jonsterling over 6 years ago
Labels: wontfix, Thought

#416 - Cache the locations of redlib files

Issue - State: closed - Opened by favonia over 6 years ago

#410 - add tactics for box,cap

Issue - State: closed - Opened by ecavallo over 6 years ago - 5 comments
Labels: enhancement, elaborator

#409 - Private data types

Issue - State: open - Opened by favonia over 6 years ago

#403 - Vim highlighting weirdness

Issue - State: closed - Opened by favonia over 6 years ago
Labels: bug, editor

#402 - Resolution of constructor names

Issue - State: open - Opened by favonia over 6 years ago - 2 comments

#401 - Module for indentation/printing

Issue - State: closed - Opened by favonia over 6 years ago

#392 - Informal description of the rot files

Issue - State: closed - Opened by favonia over 6 years ago - 1 comment
Labels: Thought

#364 - Rename RestrictThunk

Issue - State: closed - Opened by favonia over 6 years ago
Labels: wontfix

#363 - Let equate_ty (quote_ty, equiv_ty) handle the types directly

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

#362 - [Efficiency] simultaneous, delayed substitution

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

#361 - [Efficiency] specialized, unary Quote.quote.

Issue - State: closed - Opened by favonia over 6 years ago
Labels: wontfix

#360 - Remove mortality in the coe of extension types

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

#358 - Benchmark: Map vs PersistentTable

Issue - State: closed - Opened by favonia over 6 years ago

#356 - Consider adding records (including the optimization of non-dependency)

Issue - State: closed - Opened by favonia over 6 years ago

#355 - Add non-dependent pair types

Issue - State: closed - Opened by favonia over 6 years ago

#354 - Add non-dependent function types

Issue - State: closed - Opened by favonia over 6 years ago

#349 - Not very correct name printing

Pull Request - State: closed - Opened by favonia over 6 years ago - 1 comment

#345 - Consider adding a new class for volatile terms in addition to commands and constructors

Issue - State: closed - Opened by favonia over 6 years ago - 5 comments
Labels: typechecker

#344 - The Moebius boundary

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

#341 - Short circuit the construction of ghcom to the Extreme

Issue - State: closed - Opened by favonia over 6 years ago

#339 - Clean up code about V

Pull Request - State: closed - Opened by favonia over 6 years ago - 1 comment

#331 - System rectification campaign

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

#330 - Non-local validity

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

#327 - Avoid re-typechecking

Issue - State: closed - Opened by favonia over 6 years ago - 2 comments
Labels: bug, typechecker

#325 - check_tm_sys is re-evaluating the same face multiple times

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

#292 - Make pretypes directly accessible to users

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

#271 - Remove false faces as soon as possible

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

#270 - New redtt core

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

#268 - Idea: let Quote control unfolding

Issue - State: open - Opened by jonsterling over 6 years ago - 4 comments

#232 - Immortal rot file format

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

#156 - Mortal spaces in pretty printing

Issue - State: closed - Opened by favonia over 6 years ago - 3 comments
Labels: bug, help wanted

#152 - Change the programming style of Cx.def and Cx.ext_blah

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

#147 - Make movie posters

Issue - State: closed - Opened by favonia over 6 years ago
Labels: enhancement, help wanted, notes

#143 - consistent identifier naming scheme for .red files

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

#132 - The SPLIT_COERCION algorithm needs some love.

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

#102 - Later Modality

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

#101 - coe of V, for real!

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

#100 - Cubical Inductive Types

Issue - State: closed - Opened by jonsterling over 6 years ago - 2 comments

#99 - source positions in surface language

Issue - State: closed - Opened by jonsterling over 6 years ago - 3 comments

#98 - Scope bug somewhere ;-)

Issue - State: closed - Opened by jonsterling over 6 years ago - 2 comments
Labels: bug

GitHub / redprl/redtt issues and pull requests