Closed UlfNorell closed 10 years ago
From nils.anders.danielsson on September 17, 2013 03:17:41
Owner: andreas....@gmail.com
From andreas....@gmail.com on October 21, 2013 14:04:46
Sounds reasonable. One more equality check here does not hurt...
Status: Accepted
Owner: ---
Cc: dominique.devriese@gmail.com
Labels: Instance Type-Enhancement Priority-High
From andreas....@gmail.com on November 07, 2013 14:21:18
Thu Nov 7 23:18:53 CET 2013 Andreas Abel andreas.abel@ifi.lmu.de
Owner: andreas....@gmail.com
From andreas....@gmail.com on November 07, 2013 14:21:48
Status: Fixed
From guillaum...@gmail.com on September 12, 2013 15:02:22
module Test where
postulate A B : Set f : {{ x : A }} → B a : A
a' : A a' = a
test : B test = f
{- The previous code fails with the following message:
There are indeed two values in scope of type A (a and a'), but given that they are definitionally equal, Agda should not complain about it but just pick any one of them. -}
Original issue: http://code.google.com/p/agda/issues/detail?id=899