issues
search
antitypical
/
Manifold
An implementation of a dependently-typed intermediate language used by Tesseract.
MIT License
30
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Automatic naming of encoded datatype parameters
#189
robrix
closed
8 years ago
0
Abstract binding trees
#188
robrix
closed
8 years ago
2
Typechecking fails for eliminations of values of computed types
#187
robrix
opened
8 years ago
0
Error messages have no source info
#186
robrix
opened
8 years ago
0
Modules can contain `Implicit` types and values
#185
robrix
opened
8 years ago
0
Propositional equality
#184
robrix
closed
8 years ago
0
[WIP] Diff entire types
#183
robrix
opened
8 years ago
0
Expected/actual types are shown out of context
#182
robrix
opened
8 years ago
0
Expected/actual types are hard to read
#181
robrix
opened
8 years ago
0
Some type parameters cannot be inferred
#180
robrix
opened
8 years ago
0
Unification
#179
robrix
closed
8 years ago
1
Sigma.second is ill-typed
#178
robrix
closed
8 years ago
0
Arbitrary Terms don’t get shrunk
#177
robrix
opened
8 years ago
0
Pretty-print well-known embedded term values as “literals”
#176
robrix
opened
8 years ago
1
Evaluation (& substitution?) produces ill-typed normal forms
#175
robrix
closed
8 years ago
0
Embedded terms
#174
robrix
closed
8 years ago
2
Module dependencies are imported transitively
#173
robrix
opened
8 years ago
1
[WIP] Datatype descriptions
#172
robrix
opened
8 years ago
0
Represent typechecking errors as annotated terms
#171
robrix
opened
8 years ago
2
Lazy cata/paramorphisms
#170
robrix
closed
8 years ago
1
AnnotatedTerm annotations are mutable.
#169
robrix
closed
8 years ago
0
Replace `Term` with a typealias of `AnnotatedTerm<()>`
#168
robrix
opened
8 years ago
1
Arbitrary annotations
#167
robrix
closed
8 years ago
0
Construct modules with definitions
#166
robrix
closed
8 years ago
0
Module is CustomStringConvertible.
#165
robrix
closed
8 years ago
0
Generalize Elaborated to arbitrary expression annotations
#164
robrix
closed
8 years ago
0
Elaborate terms in modules
#163
robrix
opened
8 years ago
1
Definitional equality returns a term
#162
robrix
closed
8 years ago
0
Implicit parameters
#161
robrix
closed
8 years ago
0
Type erasure
#160
robrix
opened
8 years ago
1
Ad hoc compilation strategies
#159
robrix
opened
8 years ago
0
Compilation
#158
robrix
opened
8 years ago
0
Evaluation throws
#157
robrix
closed
8 years ago
0
Unicode synonyms for construction operators?
#156
robrix
closed
8 years ago
1
Implicit arguments
#155
robrix
closed
8 years ago
3
Functor typeclass as a type
#154
robrix
closed
8 years ago
1
Gather modules & their tests together
#153
robrix
closed
8 years ago
0
Optional type annotations in lambdas
#152
robrix
closed
8 years ago
0
Remove `TermType`.
#151
robrix
closed
8 years ago
0
Functor “typeclass” as type whose inhabitants are the typeclass “instances”
#150
robrix
closed
8 years ago
0
Oh
#149
robrix
closed
8 years ago
1
Type is no longer in Type.
#148
robrix
closed
8 years ago
0
Trim
#147
robrix
closed
8 years ago
0
Finite sets
#146
robrix
closed
8 years ago
0
Vectors, redux
#145
robrix
closed
8 years ago
0
What is Leibniz equality? What is it for?
#144
robrix
opened
8 years ago
2
Vectors
#143
robrix
closed
8 years ago
0
Encoded datatypes
#142
robrix
closed
8 years ago
0
Church-encoded lists
#141
robrix
closed
8 years ago
0
Fewer parentheses
#140
robrix
closed
8 years ago
0
Next