Closed UlfNorell closed 10 years ago
From pumpkingod@gmail.com on September 28, 2013 17:02:09
By using the decision procedure and False, Agda can infer the proof for you in many cases. If I write literal arguments to divMod, or I have a suc of anything, the proof will be inferred. The standard equality won't ever be inferred.
From mech...@botik.ru on September 29, 2013 04:03:00
Can you, please, explain more definitely?
1) > or I have a suc of anything, the proof will be inferred.
open import Relation.Nullary.Decidable using (False) open import Relation.Binary using (DecTotalOrder; module DecTotalOrder) open import Relation.Binary.PropositionalEquality using (≢) open import Data.Nat using (ℕ; suc) renaming (decTotalOrder to natDTO) open import Data.Nat.DivMod using (divMod)
open DecTotalOrder natDTO using (≟) postulate anything : ∀ {a} {A : Set a} → A
rd = 5 divMod 2 rd2 = 5 divMod (suc anything)
lemma : (suc anything) ≢ 0
Everithing here is type-checked.
`lemma' is also type-checked, despite that it uses ≢ instead of False. So, why do we need using False ?
2) What is a literal argument? Is it possble '4' divMod '2' ?
From pumpkingod@gmail.com on October 07, 2013 18:53:57
Note that in your example, you didn't have to pass a proof that 2 was not 0 to your calls to divMod in rd or rd2. Now try doing as you suggest and replacing the False ... with the actual proof, leaving the argument implicit, and try again. Also experiment with what happens if you pass 0 as the second argument to divMod.
From nils.anders.danielsson on October 30, 2013 02:31:56
Status: WontFix
From mech...@botik.ru on September 20, 2013 20:56:58
Standard library lib-0.7 writes in several places in Data.Nat.DivMod the type
False (divisor ≟ 0),
while divisor ≢ 0 looks more natural to use (the corresponding code modification will be needed).
Am I missing something?
Original issue: http://code.google.com/p/agda/issues/detail?id=910