Idris2

Idris2 copied to clipboard

[ new ] Enable REPL reload command to reload ipkgs

2

Enables REPL `:reload` command to reload entire ipkgs.

skykanin

confusing error message for unannotated definition in `where` block attached to polymorphic function

1

```idris two: Nat two = 2 bar: a -> a bar x = x where wat = two ``` yields the error message: ``` While processing right hand side of...

rntz

```idris bar = 3 where wat = 2 baz = 3 where wat = 2 ``` Produces the error: ``` While processing right hand side of baz. Main.wat is already...

rntz

With Idris 2, version 0.5.1-68a144bf1. The following code: ``` interface Cat obj (hom: obj -> obj -> Type) where id : hom a a ``` produces the error: ``` While...

rntz

The tutorial page on "Interactive Editing" (https://idris2.readthedocs.io/en/latest/tutorial/interactive.html) claims the idris2 repl supports a command `:addmissing` (synonym `:am`). As far as I can tell it does not. It is not listed...

rntz

# Context `%default` pragma, to my knowledge, acts from the next line till the next such pragma or till the end of file. Thus, this typechecks ```idris %default covering f...

buzden

There are only two topics currently, but why not dream big? This PR also remfinal newline when printing usage.

iacore

AddClause doesn't work right with a function following an interface implementation in a mutual clause

2

https://gist.github.com/redfish64/4ca71b907917f74149077bc57e1a9adf ``` interface Foo38 x where foo38 : x -> Int mutual Foo38 String where foo38 x = 42 foo39 : Bool -> Int --run AddClause on foo39 -- returns:...

redfish64

Possible issue with shrinkTerm?

1

I'm not certain if this is expected/desired behavior or not. Currently, when `shrinkTerm` encounters a metavariable, it fails if any argument is not in the smaller context: https://github.com/idris-lang/Idris2/blob/891b2d667ab9ef2f12aaaf372494ad680a494be5/src/Core/TT.idr#L1086-L1093 This is...

mb64

Creates a case where you don't use the results fails to type check sometimes

3

This simple example is causing a problem for me, since if I use code resembling monad bind often the result gets ignored (ie. >>) , and so this issue crops...

redfish64