idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-05 23:18:06 +03:00
Code Issues Projects Releases Wiki Activity
b03395debe
Idris2/libs/base/Data
History
Guillaume ALLAIS 13ef8ba707 [ fix #1782 ] remove the case-specific code 
I can't make sense of this code, it seems to try to convert the
case function corresponding to `let (a, b) = f n in ...` into a
different case function where `f n` and `(a, b)` have been unified.
But if `f n` is a bona fide stuck computation, there's no chance of
this happening.

Just turning this off solves the #1782 and only breaks one function
in the whole of the idris2 repo (I would have expected our current
termination oracle to be too weak to detect it as valid anyway!)
and one in frex (which, again, should not have been seen as terminating).

Also fixes #1460
2021-07-26 17:03:16 +01:00
..
Bool Add some algebra implementations 2020-07-17 08:25:20 -05:00
Fin Define and implement Relation interfaces (#1472) 2021-07-09 09:06:27 +01:00
IOArray Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
List Define and implement Relation interfaces (#1472) 2021-07-09 09:06:27 +01:00
Nat Use Not instead of -> Void (#1667) 2021-07-13 15:32:01 +01:00
Primitives Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
SnocList module Data.SnocList.Elem (#1478) 2021-06-28 20:34:39 +01:00
Vect Use Not instead of -> Void (#1667) 2021-07-13 15:32:01 +01:00
Bifoldable.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
Bits.idr [ new ] Missing integer type interfaces (#1629) 2021-06-28 20:00:10 +01:00
Bool.idr Use Not instead of -> Void (#1667) 2021-07-13 15:32:01 +01:00
Buffer.idr Merge branch 'master' into refc-buffer 2021-07-16 09:44:40 +01:00
Colist1.idr Cleanup List1 (#1091) 2021-03-17 14:07:52 +00:00
Colist.idr [ base ] Some lacking implementations for Uninhabited were added 2021-06-15 15:07:54 +03:00
Contravariant.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
DPair.idr [ new ] Interface implementations for Subset 2021-03-09 11:25:03 +00:00
Either.idr Add Bifunctor interface (#701) 2020-09-30 10:51:07 +01:00
Fin.idr [ base ] add List functions (#1550) 2021-07-01 08:00:12 +01:00
Fuel.idr [ new ] Proof search from 'Applications of Applicative Proof Search' (#1093) 2021-03-01 08:29:43 +00:00
Fun.idr Some cleanup was done. Changed code is mosly equivalent to the former. 2021-02-16 19:05:33 +00:00
IOArray.idr Return Bool from IOArray.writeArray 2021-07-15 22:16:22 +01:00
IORef.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
List1.idr [ fix #1782 ] remove the case-specific code 2021-07-26 17:03:16 +01:00
List.idr [ base ] add List functions (#1550) 2021-07-01 08:00:12 +01:00
Maybe.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
Morphisms.idr Simplify some lambdas (#1561) 2021-06-16 15:22:30 +01:00
Nat.idr Define and implement Relation interfaces (#1472) 2021-07-09 09:06:27 +01:00
Ref.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
Rel.idr Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
SnocList.idr [ base ] add List functions (#1550) 2021-07-01 08:00:12 +01:00
So.idr [ fix #899 ] Be careful when generating an impossible LHS (#1081) 2021-02-22 09:53:30 +00:00
Stream.idr [ fix #1581 ] public export Range functions and implementations (#1602) 2021-06-28 16:52:23 +01:00
String.idr Change semantics of lines and unlines function to match Haskell and other languages (#1585) 2021-07-17 14:54:23 +01:00
These.idr [ new ] Add Bifoldable and Bitraversable interfaces to Prelude (#1265) 2021-04-08 17:25:37 +01:00
Vect.idr Make drop and drop' public exported from the vect module. 2021-07-20 14:27:43 +01:00
Zippable.idr Make zip infixr 6 2021-02-23 10:54:28 +00:00