Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / owo-lang/minitt-rs issues and pull requests

#26 - Try apply `id` to `id`

Issue - State: closed - Opened by xieyuheng over 5 years ago - 2 comments
Labels: available-in-voile, discussion

#25 - Try the `elimBool` of the paper.

Issue - State: closed - Opened by xieyuheng over 5 years ago - 6 comments
Labels: bug, discussion

#24 - Create `minitt-util`

Issue - State: closed - Opened by ice1000 over 5 years ago - 1 comment

#23 - Use KaTeX in rustdoc

Issue - State: closed - Opened by ice1000 almost 6 years ago - 1 comment
Labels: enhancement

#22 - Entering empty expressions in REPL mode should not trigger parsing

Issue - State: closed - Opened by anqurvanillapy almost 6 years ago
Labels: enhancement

#21 - level

Pull Request - State: closed - Opened by oraluben almost 6 years ago - 1 comment
Labels: levels

#20 - Universe polymorphism

Issue - State: open - Opened by ice1000 almost 6 years ago - 1 comment
Labels: levels, available-in-voile

#19 - [ #13 ] Level for Sigma/Pi/Sum

Pull Request - State: closed - Opened by oraluben almost 6 years ago - 3 comments
Labels: levels

#18 - merge level with new Merge feature

Pull Request - State: closed - Opened by oraluben almost 6 years ago
Labels: levels

#17 - Sum's each branch should have its own telescope

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: first-class sum

#16 - Improve `split` pretty printer

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: enhancement

#15 - Merge two sums

Issue - State: closed - Opened by ice1000 almost 6 years ago - 1 comment
Labels: first-class sum

#14 - Sigma/Pi/Sum with level

Pull Request - State: closed - Opened by oraluben almost 6 years ago - 1 comment
Labels: levels

#13 - Sum/Pi/Sigma with levels?

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: levels

#12 - The ability to attach builtin definitions (like Agda BUILTIN pragma

Issue - State: open - Opened by ice1000 almost 6 years ago
Labels: builtins

#11 - Generalized algebraic data types (indexed inductive families)

Issue - State: open - Opened by ice1000 almost 6 years ago - 22 comments
Labels: gadts

#10 - Backend framework

Issue - State: open - Opened by ice1000 almost 6 years ago
Labels: backends

#9 - Termination check (structural induction)

Issue - State: open - Opened by ice1000 almost 6 years ago - 2 comments
Labels: termination

#8 - Positivity check for sum types

Issue - State: open - Opened by ice1000 almost 6 years ago
Labels: positivity

#7 - Type universe and (possibly) universal subtyping

Issue - State: closed - Opened by ice1000 almost 6 years ago - 9 comments
Labels: subtyping, levels

#6 - Subtyping check on sum types

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: first-class sum

#5 - Default placeholder for constructor parameter/pattern

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: syntactic sugar

#4 - `const` parser

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: syntactic sugar

#3 - Infer type of constructor call as a "minimum sum"

Issue - State: closed - Opened by ice1000 almost 6 years ago
Labels: first-class sum

#2 - Support "otherwise" in split

Issue - State: open - Opened by ice1000 almost 6 years ago
Labels: first-class split, available-in-voile

#1 - Support big lambdas

Issue - State: closed - Opened by ice1000 almost 6 years ago - 2 comments
Labels: enhancement