aya-prover/aya-dev

Issues

• Revise when we have signature for classes

  #1132 opened 5 months ago by ice1000
  0

• Coercive subtyping didn't work from path to functions. WTF?

  #1130 opened 5 months ago by ice1000
  1

• Pretty print JIT-compiled core definitions

  #1128 opened 5 months ago by ice1000
  0

• Implement `:i` in repl

  #1125 opened 5 months ago by ice1000
  0

• More Faithful Highlight

  #1121 opened 5 months ago by HoshinoTented
  0

• Matching.bindCount

  #1066 opened 6 months ago by ice1000
  0

• Type Infering

  #942 opened 6 months ago by HoshinoTented
  2

• Correctly implement coe on pi

  #1037 opened 7 months ago by ice1000
  0

• Compile sigma type term

  #1033 opened 6 months ago by ice1000
  2

• More efficient pretty printer

  #1034 opened 6 months ago by ice1000
  1

• Usage analy in compiler, generate constant closures when possible

  #1032 opened 6 months ago by ice1000
  0

• ISE

  #1101 opened 6 months ago by ice1000
  1

• Compiler Optimization

  #1031 opened 6 months ago by HoshinoTented
  1

• Callable.Tele with empty args could have a shared instance

  #1099 opened 6 months ago by ice1000
  2

• Context-based name generator

  #1041 opened 6 months ago by ice1000
  0

• Cringe error report

  #1079 opened 6 months ago by ice1000
  0

• Report error if the variables in `elim` is unresolved or resolved to somewhere else

  #1036 opened 6 months ago by ice1000
  2

• Re #562

  #1081 opened 6 months ago by ice1000
  1

• `IndexOutOfBoundsException` when parsing result types

  #1015 opened 6 months ago by dannypsnl
  4

• Once we're up to lowercase package names, `data` conflict with the keyword

  #1069 opened 6 months ago by ice1000
  1

• Re #564

  #1061 opened 6 months ago by ice1000
  1

• Re #751

  #1060 opened 6 months ago by ice1000
  2

• selfTeleSize

  #1065 opened 6 months ago by ice1000
  0

• ??? NPE

  #1058 opened 6 months ago by ice1000
  1

• NullPointerException

  #1056 opened 6 months ago by ice1000
  1

• Compile prim def and prim calls

  #1030 opened 6 months ago by ice1000
  1

• Implement boundary separation

  #1040 opened 6 months ago by ice1000
  0

• Constraints in the type checker

  #1039 opened 7 months ago by ice1000
  1

• Implement compCCHM

  #1038 opened 7 months ago by ice1000
  0

• Report error if a pattern matching function's signature uses itself

  #1035 opened 6 months ago by ice1000
  0

• Implement hcomp

  #1029 opened 7 months ago by ice1000
  0

• bors is dead, what to do? Enable GHMQ?

  #1010 opened 6 months ago by ice1000
  4

• Container image for Aya

  #1024 opened a year ago by WojciechKarpiel
  5

• Wrong URL to CI badge

  #1020 opened a year ago by skylee03
  0

• Crash with `InternalException` after report an error

  #1016 opened a year ago by dannypsnl
  3

• Goal didn't give reasonable types

  #1013 opened a year ago by dannypsnl
  1

• DSL for generating highlighted contents

  #1004 opened a year ago by ice1000
  0

• StackOverflow

  #1000 opened a year ago by HoshinoTented
  1

• We need a better literate backend for academic writing

  #953 opened 2 years ago by imkiva
  4

• InternalException about Generalized Variables

  #972 opened 2 years ago by HoshinoTented
  4

• `aya-hidden` is printed to tex

  #969 opened 2 years ago by imkiva
  2

• Markdown backend bug

  #950 opened 2 years ago by imkiva
  1

• We should develop our own IDE

  #949 opened 2 years ago by ice1000
  6

• `atob` seems broken in vuepress

  #951 opened 2 years ago by imkiva
  7

• Bad Meta

  #944 opened 2 years ago by HoshinoTented
  7

• Fully predicative termination checker

  #940 opened 2 years ago by ice1000
  0

• Literate mode bug?

  #937 opened 2 years ago by imkiva
  2

• We should use `enum X { Obj; }` for singletons!

  #930 opened 2 years ago by ice1000
  1

• Unification bug

  #924 opened 2 years ago by ice1000
  0

• Coverage checker bug

  #914 opened 2 years ago by ice1000
  3