Issues

• Parentheses around infix operator reported as redundant

  bug
  arend-lang/Arend#158 · Filter by author WPaupa opened on Sep 26, 2026
  1

  

• Proof of Empty without axioms: constructor conditions are ignored when deciding emptiness and coverage

  bugmajor
  arend-lang/Arend#154 · Filter by author Bibin112358 opened on Sep 18, 2026
  

• java.lang.IllegalStateException: WriteIntentReadAction can not be called from ReadAction

  bug
  arend-lang/Arend#153 · Filter by author sxhya opened on Sep 8, 2026

• Make levels visible in a where block

  arend-lang/Arend#151 · Filter by author WPaupa opened on Sep 6, 2026

• Infix notation inconsistency

  arend-lang/Arend#145 · Filter by author WPaupa opened on Aug 13, 2026

• Misleading 'Cannot find subexpression' from rewrite: reported Expression contains the pattern it says is missing

  usability problem
  arend-lang/Arend#141 · Filter by author sxhya opened on Aug 11, 2026

• Implement CLI formatter

  enhancement
  arend-lang/Arend#135 · Filter by author sxhya opened on Aug 3, 2026
  

• -ps --bodies: show how each proof-search hit is actually proved

  enhancementusability problem
  arend-lang/Arend#133 · Filter by author sxhya opened on Aug 3, 2026
  1

• Same type mismatch

  arend-lang/Arend#127 · Filter by author WPaupa opened on Jun 16, 2026
  

• Instance resolution and the reduction model are fragile and hard to introspect

  arend-lang/Arend#126 · Filter by author sxhya opened on Jun 3, 2026

• Tactics should work with casts freely

  enhancement
  arend-lang/Arend#124 · Filter by author sxhya opened on May 29, 2026
  

• Create field_simp tactic

  enhancement
  arend-lang/Arend#121 · Filter by author sxhya opened on May 23, 2026
  

• RealField instance inference hints

  Feature

  arend-lang/Arend#120 · Filter by author part-xx opened on May 21, 2026
  

• Reload Arend libraries from Intellij does not force reload of library extensions (e.g. metas)

  bug
  arend-lang/Arend#119 · Filter by author sxhya opened on May 20, 2026
  

• Implicit-Array inference failure on BigSum-ldistr / BigSum-ext / BigSum_+ reports as Ring-instance failure on the **enclosing lemma's signature**

  arend-lang/Arend#118 · Filter by author sxhya opened on May 19, 2026

• equation.cRing and linarith cannot find Real's class instance from a bare goal

  bug
  arend-lang/Arend#117 · Filter by author sxhya opened on May 18, 2026
  

• Type-mismatch pretty-printer mixes short and qualified flavors of the same type

  arend-lang/Arend#114 · Filter by author sxhya opened on May 13, 2026

• equation.cRing silently falls back when the CRing instance is out of scope

  arend-lang/Arend#113 · Filter by author sxhya opened on May 13, 2026

• Empty pattern matching on strings compiles

  arend-lang/Arend#111 · Filter by author WPaupa opened on May 12, 2026
  

• linarith doesn't unfold truncated subtraction -'

  bug
  arend-lang/Arend#110 · Filter by author sxhya opened on May 11, 2026
  

• Inconsistent ConcreteGroup Construction Between Console and IntelliJ Proof Search

  invalidquestion
  arend-lang/Arend#98 · Filter by author sxhya opened on Apr 1, 2026

• Tasks for @valis

  arend-lang/Arend#92 · Filter by author sxhya opened on Mar 24, 2026
  

• PsiInvalidElementAccessException after some portion of erroneous code has been removed

  arend-lang/Arend#90 · Filter by author sxhya opened on Mar 21, 2026

• HighlightInfo is incorrectly stored or reused

  bug
  arend-lang/Arend#89 · Filter by author sxhya opened on Mar 20, 2026
  2

• Linarith has problems detecting superfluous premises

  bug
  arend-lang/Arend#86 · Filter by author sxhya opened on Mar 17, 2026