JetBrains/Arend

Issues

• Exception in thread "main" java.lang.IllegalStateException

  #345 opened 2 months ago by sxhya
  0

• NPE because "thisExpr" is null

  #344 opened 2 months ago by sxhya
  0

• Tutorial for "Console Application" Turning Up Error

  #343 opened 2 months ago by brandon-sisler
  2

• No error reported about wrong use of `\use \coerce`

  #342 opened 3 months ago by sxhya
  0

• Usability problem with inheritance of classes with external parameters.

  #340 opened 5 months ago by sxhya
  1

• Problem with mixing `this` with external parameters

  #338 opened 5 months ago by sxhya
  1

• StackOverflowError

  #341 opened 5 months ago by sxhya
  0

• Problem with mixing constructors defined via pattern-matching with external parameters

  #339 opened 5 months ago by sxhya
  0

• Auto-implicits in \where block stops working under function defined as a full pat mat

  #337 opened a year ago by Odomontois
  1

• :lib command not working as expected.

  #336 opened a year ago by sxhya
  0

• Issues with Console REPL

  #333 opened a year ago by sxhya
  0

• Improve console REPL completion

  #334 opened a year ago by sxhya
  2

• Allow multiline input in REPL

  #335 opened a year ago by sxhya
  0

• Wrong scopes for `\data` defined with `\with` construction

  #332 opened a year ago by sxhya
  1

• PrettyPrintOptions button is greyed out

  #331 opened a year ago by sxhya
  0

• A bug in unification

  #304 opened 2 years ago by ice1000
  3

• AssertionError in UnparsedConstructorPattern

  #328 opened 2 years ago by valis
  0

• Allow matching infix constructors in patterns

  #319 opened 2 years ago by marat-rkh
  4

• NPE during typechecking goal with arguments

  #322 opened 2 years ago by marat-rkh
  2

• Strange behavior of a Pi-typed goal

  #321 opened 3 years ago by knisht
  1

• IllegalArgumentException

  #317 opened 3 years ago by knisht
  0

• Minimization of expression (Ob {D}) is likely diverged

  #311 opened 3 years ago by valis
  1

• Different equality types treated as the same in typechecking

  #302 opened 3 years ago by ShreckYe
  1

• Applying `\func t<-helper {x y : Nat} (p : T (x < y)) : T (x < suc y)` repeatedly always typechecks

  #301 opened 3 years ago by ShreckYe
  0

• Add metas for \Pi, similar to metas for \Sigma

  #300 opened 3 years ago by marat-rkh
  3

• Allow more unicode symbols in aliases

  #299 opened 3 years ago by marat-rkh
  3

• NPE in level solver

  #298 opened 3 years ago by knisht
  0

• Dynamic definitions for `\data`

  #297 opened 3 years ago by tonyxty
  0

• NPE in typechecking

  #296 opened 3 years ago by marat-rkh
  2

• Equality of any inhabitant of t = t with idp pass type checking.

  #295 opened 3 years ago by ilhikki
  2

• Reorder declarations in Prelude.ard

  #292 opened 3 years ago by marat-rkh
  2

• Arend forces splitting on unnecessary variables

  #286 opened 4 years ago by ice1000
  1

• Allow pattern matching on idp for \case expressions

  #294 opened 4 years ago by knisht
  1

• Import existing imports in REPL

  #291 opened 4 years ago by valis
  0

• Add documentation comments to Prelude.ard

  #293 opened 4 years ago by marat-rkh
  0

• Bottom is accidentally provable

  #290 opened 4 years ago by knisht
  1

• \let definitions in REPL

  #289 opened 4 years ago by valis
  2

• Dependencies upgrade before 1.6 release

  #277 opened 4 years ago by ice1000
  2

• Conditions referring to the current constructor?

  #288 opened 4 years ago by ice1000
  0

• A plugin error happens with new IDEA

  #287 opened 4 years ago by zhelenskiy
  2

• Computation stucked with new Fin from Prelude

  #285 opened 4 years ago by knisht
  0

• Termination checker is sensitive to let-bindings

  #284 opened 4 years ago by knisht
  2

• Positivity checker complains in an unexpected place

  #283 opened 4 years ago by knisht
  1

• Built-in finite sets

  #274 opened 4 years ago by valis
  5

• Duplicating clauses in pattern matching

  #281 opened 4 years ago by knisht
  0

• Internal error with aliases after \extends keyword

  #280 opened 4 years ago by knisht
  0

• New Fin from Prelude lacks computational properties

  #282 opened 4 years ago by knisht
  0

• Arend REPL crashes with CCE

  #279 opened 4 years ago by knisht
  0

• ISE in CorrespondedSubExprVisitor

  #278 opened 4 years ago by valis
  0

• Module with parameters

  #276 opened 4 years ago by ice1000
  3