wwww

Idris ver 1.3.2-git:9549d9cb9 # Steps to Reproduce Check the following for totality via: :total foo ``` data Id a = MkId a foo : (f : List a) -> Id...

Either the general definition for Integral is wrong, or too permissive: `(Integral a, Ord a, Neg a) => Range a where ...` # Steps to Reproduce `[the Bits32 10, 5...

# Steps to Reproduce ```idris module Main namespace Foo1 foo : Nat -> () foo k1 = ?foo1_rhs namespace Foo2 export foo2 : Nat -> () foo2 k2 = ?foo2_rhs...

linear lambda claims to consume unrelated binder

5

Idris 2, version 0.1.0-b617cae88 # Steps to Reproduce ```idris foo1 : (1 f : (1 x : a) -> b) -> Maybe Char foo1 f = Just 'c' >>= (\arr...

Idris 2, version 0.1.0-19426ecd1 I've included a lambda of case and a lambdacase to show it's not specific to one. # Steps to Reproduce ```idris foo1 : () foo1 =...

It would be useful to have a way, in patterns, to check for the presence of a constructor without regard to its arguments. Currently given ```idris data Tree : Type...

Duplicate pattern cases have a very unclear error message. Ran into this while writing a tree but the simpler case is shown here. # Steps to Reproduce typecheck: ```idris module...

… checks