Issues

• Reduction of hcom

  cubical
  aya-prover/aya-dev#1467 · Filter by author ice1000 opened on Sep 25, 2026

• Search global instances using instance case tree

  classes
  aya-prover/aya-dev#1439 · Filter by author ice1000 opened on Nov 25, 2025 · v0.42

• Investigate the feasibility to rewrite descent to be monadic

  Task

  aya-prover/aya-dev#1436 · Filter by author ice1000 opened on Nov 21, 2025

• More informative normalization result type and better conversion check

  Task

  aya-prover/aya-dev#1435 · Filter by author ice1000 opened on Nov 20, 2025

• Don't panic when Expr.Hole holds bad things

  featureresolving
  aya-prover/aya-dev#1370 · Filter by author HoshinoTented opened on Sep 5, 2025

• Blocked meta equation is not delayed but rejected

  bugmeta variablestracking
  aya-prover/aya-dev#1358 · Filter by author HoshinoTented opened on May 29, 2025
  2

  

• Leftover of #1354: module-based completion, tests

  lsp
  aya-prover/aya-dev#1355 · Filter by author ice1000 opened on May 3, 2025

• A repl command to run double checker on a function definition

  developer experiencedouble checkerrepl
  aya-prover/aya-dev#1337 · Filter by author ice1000 opened on Apr 7, 2025
  2

• Meaningful LocalVariableTable metadata for JIT-compiled classfile

  developer experiencejit
  Feature

  aya-prover/aya-dev#1329 · Filter by author linxuanm opened on Feb 18, 2025
  1

  

• Implement pruning to fix this example by Hoshino

  bugmeta variablestracking
  Feature

  aya-prover/aya-dev#1295 · Filter by author ice1000 opened on Jan 29, 2025
  1

• Shapes of list join and list concat

  shape
  Feature

  aya-prover/aya-dev#1294 · Filter by author ice1000 opened on Jan 28, 2025

• Dead code elimination

  performanceserialization
  Feature

  aya-prover/aya-dev#1284 · Filter by author ice1000 opened on Jan 22, 2025

• Make a core version of variable, check them, and introduce dependencies in stmt tycker

  generalizationresolving
  Feature

  aya-prover/aya-dev#1220 · Filter by author ice1000 opened on Dec 15, 2024
  

• Case Tree for Non-Overlap Pattern Matching

  core: patternfeatureperformance
  Task

  aya-prover/aya-dev#1208 · Filter by author HoshinoTented opened on Dec 11, 2024
  1

  

• When array exprs solve their types, the element type info is not propagated to the terms

  meta variables
  Task

  aya-prover/aya-dev#1146 · Filter by author ice1000 opened on Nov 18, 2024
  3

• Revise when we have signature for classes

  classes
  Task

  aya-prover/aya-dev#1132 · Filter by author ice1000 opened on Jul 12, 2024

• More Faithful Highlight

  pretty print
  aya-prover/aya-dev#1121 · Filter by author HoshinoTented opened on Jun 22, 2024

• Implement boundary separation

  cubicaluip
  Task

  aya-prover/aya-dev#1040 · Filter by author ice1000 opened on May 18, 2024

• Implement com

  cubical
  Task

  aya-prover/aya-dev#1038 · Filter by author ice1000 opened on May 5, 2024 · v0.42

• Container image for Aya

  good first issue
  aya-prover/aya-dev#1024 · Filter by author WojciechKarpiel opened on Dec 29, 2023
  5

• StackOverflow

  bug
  Bug

  aya-prover/aya-dev#1000 · Filter by author HoshinoTented opened on Oct 1, 2023
  3

• We need a better literate backend for academic writing

  question
  aya-prover/aya-dev#953 · Filter by author imkiva opened on Apr 3, 2023
  4

• Fully predicative termination checker

  terck
  aya-prover/aya-dev#940 · Filter by author ice1000 opened on Mar 1, 2023

• Positivity check is incorrectly implemented

  positivity
  aya-prover/aya-dev#849 · Filter by author ice1000 opened on Dec 21, 2022
  3

  

• Create a github repo for stdlib?

  aya-prover/aya-dev#834 · Filter by author mio-19 opened on Dec 17, 2022
  1