issues
search
aya-prover
/
aya-prover-proto
┗:smiley:┛ ┏:smiley:┓ ┗:smiley:┛
GNU General Public License v3.0
11
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Docs
#763
ice1000
closed
2 years ago
0
Fix struct
#762
ice1000
closed
2 years ago
0
Rename in `new` expression field telescopes
#761
ice1000
closed
2 years ago
0
Address some IDE inspections
#760
ice1000
closed
2 years ago
0
Fix record substitution
#759
ice1000
closed
2 years ago
0
Make `AppExpr` Binary
#758
tonfeiz
closed
2 years ago
34
Report conditions in goal
#757
wsx-ucb
closed
2 years ago
4
Failed to type check some path expression
#756
wsx-ucb
closed
2 years ago
4
No longer need to substitute telescope
#755
ice1000
closed
2 years ago
0
Slightly optimize the pretty printer
#754
ice1000
closed
2 years ago
14
Pretty printing this code is extremely slow
#753
ice1000
closed
2 years ago
20
Heartbreaker
#752
ice1000
closed
2 years ago
0
Heartbroken
#751
ice1000
closed
2 years ago
0
Insert implicits in `new` expression
#749
dark-flames
closed
2 years ago
4
Improve goal error message
#748
ice1000
closed
2 years ago
0
Enhanced goal error message
#747
ice1000
closed
2 years ago
1
Some follow-up changes
#745
ice1000
closed
2 years ago
2
Enhance coverage checker
#744
ice1000
closed
2 years ago
0
Bug in OOP confluence
#743
ice1000
closed
2 years ago
6
Error messages for confluence checker enhancement
#742
ice1000
closed
2 years ago
6
Allow omitting (some) `impossible` clauses
#741
ice1000
closed
2 years ago
1
More test cases
#740
ice1000
closed
2 years ago
0
Make `AppExpr` binary
#739
ice1000
closed
2 years ago
32
Many things about levels
#738
ice1000
closed
2 years ago
0
Fix comment lexical rules
#737
ice1000
closed
2 years ago
0
`new` expression should try to insert implicits
#736
ice1000
closed
2 years ago
0
TermToPat to pattern match
#735
ice1000
closed
2 years ago
0
Refactor UntypedDefEq.java and TypedDefEq.java
#734
ericwang385
closed
2 years ago
3
Explicitly pass level arguments in fncall/datacall/structcall expressions
#732
ice1000
closed
2 years ago
1
Underscore syntax for level arguments
#731
ice1000
closed
2 years ago
12
Perform missing level substitution
#730
ice1000
closed
2 years ago
0
Levels are wrongly generated
#729
ice1000
closed
2 years ago
0
Generated pi types have omega level, bad bad
#728
ice1000
closed
2 years ago
2
Fix pretty print, add some tests
#727
ice1000
closed
2 years ago
0
Eta conversion in `new` fields
#726
ice1000
closed
2 years ago
0
Darkflames code review: field substitution
#725
ice1000
closed
2 years ago
0
Level solver
#724
ice1000
closed
2 years ago
0
Inline eta* methods to uneta
#723
tonfeiz
closed
2 years ago
1
Delete some code
#721
ice1000
closed
2 years ago
1
Fix universe parsing
#720
ice1000
closed
2 years ago
0
UNETA: review suggestions
#719
ice1000
closed
2 years ago
5
Perform eta rule to check whether a term is a RefTerm
#718
tonfeiz
closed
2 years ago
9
Add fullTelescope in SubLevelDef
#716
ice1000
closed
2 years ago
0
Fix RefTerm in struct def
#715
ice1000
closed
2 years ago
0
Struct TODO fix
#714
ice1000
closed
2 years ago
0
Refactor visitTup
#713
ice1000
closed
2 years ago
3
Refactor `visitTup`
#711
ice1000
closed
2 years ago
1
Delete subproject tgbot
#710
ice1000
closed
3 years ago
0
Untyped unify when holes are present
#709
ice1000
closed
3 years ago
0
Report `UnexpectedImplicitArgError`
#708
ice1000
closed
3 years ago
0
Next