aya-prover aya-dev issues

aya-prover / aya-dev

A proof assistant and a dependently-typed language

https://www.aya-prover.org

MIT License

281 stars 16 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Compiled binary should be used right after being generated

#1151 ice1000 opened 1 day ago
0
Turn `SigmaTerm` binary

#1150 ice1000 opened 1 day ago
0
The ability to disable the default import of `prelude`?

#1149 ice1000 opened 1 day ago
0
Error handling, handle `RuleReducer.Con` in `visibleArgs` in `CorePrettier`

#1148 ice1000 closed 1 day ago
1
Fix two issues related to arrays and meta lit terms, implement `debug-show-shapes`

#1147 ice1000 closed 1 day ago
2
When array exprs solve their types, the element type info is not propagated to the terms

#1146 ice1000 opened 1 day ago
3
Array exprs need a checking mode

#1145 ice1000 closed 1 day ago
0
List types are inferred to be the type of its elements

#1144 ice1000 closed 1 day ago
1
Illegal char `<:>` at index 0: :theKid

#1143 xianglic closed 1 day ago
1
REPL does not fully normalize treeSort

#1142 xianglic closed 1 day ago
1
Generate dummy terms

#1141 ice1000 closed 3 days ago
1
Prepare for Java 23, improve tests, fix some classes codegen errors

#1140 ice1000 closed 3 days ago
1
Jit class cp 2

#1139 ice1000 closed 3 days ago
1
Jit class cp

#1138 ice1000 closed 3 days ago
1
Reviewing Code, More Documents and Make Notes for Module System

#1137 HoshinoTented closed 3 days ago
3
Dependency upgrades

#1136 ice1000 closed 2 weeks ago
1
Refactor Module

#1135 HoshinoTented closed 2 weeks ago
7
Class resolver

#1134 ice1000 opened 3 months ago
1
Revise when we have signature for classes

#1132 ice1000 opened 4 months ago
0
Coercive subtyping fixes + cherry pick from classes

#1131 ice1000 closed 4 months ago
1
Coercive subtyping didn't work from path to functions. WTF?

#1130 ice1000 closed 4 months ago
1
Classes

#1129 ice1000 closed 4 months ago
1
Pretty print JIT-compiled core definitions

#1128 ice1000 opened 4 months ago
0
Show Information of Definition in Repl

#1127 HoshinoTented closed 4 months ago
2
Upgrade build util

#1126 ice1000 closed 4 months ago
1
Implement `:i` in repl

#1125 ice1000 closed 4 months ago
0
Do something maybe addresses Hoshino's goal

#1124 ice1000 closed 4 months ago
1
Make jlink binary compile libraries

#1123 ice1000 closed 4 months ago
1
Unify Signature with AbstractTele.Locns

#1122 HoshinoTented closed 4 months ago
1
More Faithful Highlight

#1121 HoshinoTented opened 5 months ago
0
Some error report issues reported by Utensil Song

#1120 ice1000 closed 5 months ago
1
Use closures in classes

#1119 ice1000 closed 5 months ago
1
Classes are now kinda working

#1118 ice1000 closed 5 months ago
1
Display emoji in Windows Terminal

#1117 ice1000 closed 5 months ago
1
Do not explicitly set encoding in build

#1116 ice1000 closed 5 months ago
1
Classes progress

#1115 ice1000 closed 5 months ago
1
Class progress

#1114 ice1000 closed 5 months ago
2
Class call code

#1113 ice1000 closed 5 months ago
1
Class resolve code

#1112 ice1000 closed 5 months ago
0
Release v0.33

#1111 ice1000 closed 5 months ago
1
Cleverly create bind amount, not calculate them upon jIT

#1110 ice1000 closed 5 months ago
1
Some bug fixes

#1109 ice1000 closed 5 months ago
1
Refactor the design of `Decl`, redo `TeleDecl`

#1108 ice1000 closed 5 months ago
1
Increase coverage, more code on classes

#1107 ice1000 closed 5 months ago
1
Initial `class` related code

#1106 ice1000 closed 5 months ago
2
What am I doing

#1105 ice1000 closed 5 months ago
0
Fix module name serialization

#1104 ice1000 closed 5 months ago
1
Quotient and fmset ++-assoc

#1103 ice1000 closed 5 months ago
1
Reorganize library, create `prelude`

#1102 ice1000 closed 5 months ago
1
ISE

#1101 ice1000 closed 5 months ago
1