Open UlfNorell opened 10 years ago
From andreas....@gmail.com on December 07, 2013 11:23:06
A size meta is set to i, but the user wants \inf. The early setting of this meta prevents the user from giving the goal.
Goal: Heap {i} p1 ( r1 -rank + suc (l2-rank + r2 -rank)) Have: Heap {∞} p1 ( r1 -rank + suc (l2-rank + r2 -rank))
Attachment: Issue992.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=992
From andreas....@gmail.com on December 07, 2013 11:23:06
A size meta is set to i, but the user wants \inf. The early setting of this meta prevents the user from giving the goal.
Goal: Heap {i} p1 ( r1 -rank + suc (l2-rank + r2 -rank)) Have: Heap {∞} p1 ( r1 -rank + suc (l2-rank + r2 -rank))
Attachment: Issue992.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=992