# Custom Query (358 matches)

## Results (10 - 12 of 358)

Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|

#432 | fixed | Check shadowing of rules in Inst judgement | benl | |

Description |
InstRArr looks like it's shadowed by InstRSolve. |
|||

#428 | fixed | Eliding signature in bag_toList causes type error saying existentials cannot be unified. | benl | |

Description |
bag_toList (bag: Bag a): List a = go Nil bag where -- TODO: We get a List ?41 does not match List ?91 error if we -- elide this signature. go : List a -> Bag a -> List a go xs1 BagNil = xs1 go xs1 (BagElem x) = Cons x xs1 go xs1 (BagList xs2) = go_list xs1 xs2 go xs1 (BagUnion b1 b2) = go (go xs1 b1) b2 go_list xs1 Nil = Nil go_list xs1 (Cons x xs2) = go_list (Cons x xs1) xs2 |
|||

#426 | fixed | Free existential not caught by post type check | benl | |

Description |
-- TODO: If the sig is not given we end up with a free exists which -- is not caught by the post-check. either_Functor {@x: Data}: Functor (Either x) = Functor either_fmap where either_fmap : [a b c: Data]. (b -> c) -> Either a b -> Either a c either_fmap f xx = case xx of Left xa -> Left xa Right xb -> Right (f xb) |

**Note:**See TracQuery for help on using queries.