AndrasKovacs elaboration-zoo issues

AndrasKovacs / elaboration-zoo

Minimal implementations for dependent type checking and elaboration

BSD 3-Clause "New" or "Revised" License

600 stars 34 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Why do we ignore the type while checking a hole?

#38 Hirrolot closed 8 months ago
4
Use `rhs` consistently in comments (`03-holes/Main.hs`)

#37 Hirrolot closed 9 months ago
0
Fix a couple of typos in `03-holes/Main.hs`

#36 Hirrolot closed 9 months ago
0
What does `A[spine]` mean?

#35 Hirrolot closed 8 months ago
2
Documentation of `PartialRenaming`

#34 Hirrolot closed 8 months ago
11
Fix pruning mask in function `invert`

#33 BjoernLoetters closed 9 months ago
2
Is the implementation of `invert` correct?

#32 BjoernLoetters closed 9 months ago
3
Why do we generate a fresh identifier in `quote`?

#31 Hirrolot closed 1 year ago
2
General Recursion

#30 onepunchtech opened 2 years ago
4
This example has wrong universe level, maybe remove?

#29 molikto closed 3 years ago
7
What is the need for InsertedMeta?

#28 atennapel closed 3 years ago
7
Predicative type hierarchy

#27 atennapel closed 2 years ago
1
Unification of decoding functions

#26 atennapel closed 3 years ago
6
Zoo zone for introducing inductive data types?

#25 anqurvanillapy opened 4 years ago
8
Should types be unified when unifying lambdas?

#24 atennapel closed 4 years ago
2
Adding primitives

#23 atennapel closed 3 years ago
15
Making lambda the only binder

#22 atennapel closed 4 years ago
2
How to add boolean elimination in the domain

#21 atennapel closed 4 years ago
14
Axiom for induction for church encoding

#20 atennapel closed 4 years ago
1
Get rid of all String names, only use de Bruijn

#19 AndrasKovacs closed 3 years ago
7
Stick to strict pattern unification

#18 AndrasKovacs closed 3 years ago
5
Implicit lambda insertion with deBruijn

#17 atennapel closed 4 years ago
3
Fix typo in poly-instantiation/README.md

#16 LPTK closed 4 years ago
0
How to evaluate primitive induction principles?

#15 atennapel closed 4 years ago
0
Inferring annotated lambdas

#14 atennapel closed 4 years ago
3
Eta reduction in evaluation

#13 atennapel closed 4 years ago
1
Displaying types without reducing globally defined variables

#12 atennapel closed 4 years ago
1
Elaboration seems to not handle shadows names correctly

#11 atennapel closed 4 years ago
0
What is the unification algorithm lacking in order to handle application of a meta?

#10 atennapel closed 4 years ago
6
checkSolution, should meta solution be checked?

#9 atennapel closed 4 years ago
2
Metas with reference cells

#8 atennapel closed 4 years ago
9
Anything new?

#7 ice1000 opened 4 years ago
45
Unification should check for spine length equality?

#6 atennapel closed 4 years ago
2
Some hints regarding deBruijn implementation of meta solving

#5 atennapel closed 4 years ago
6
Can you translate let-expressions to lambda abstractions?

#4 atennapel closed 5 years ago
2
Shouldn't the elaborated lambda abstractions be annotated with their parameter type?

#3 atennapel closed 5 years ago
2
Why this term fails to typecheck?

#2 VictorTaelin closed 8 years ago
4
Update nosubst.md

#1 ggreif closed 8 years ago
0