core code missing from Nat and Int#1304
Conversation
| gcd[m,n]∣n m n = transport (cong (λ a → a ∣ n) (gcdSym n m) ) (gcd[m,n]∣m n m) | ||
|
|
||
| gcd-greatest : c ∣ m → c ∣ n → c ∣ gcd m n | ||
| gcd-greatest c∣m c∣n = |
There was a problem hiding this comment.
Is there any reason why it is proved in this way, instead of currying snd (gcdIsGCD m n) c?
I tested it, and you could even write gcd-greatest = curry (snd (gcdIsGCD _ _) _), with all implicit varibles solved
| ⊥.elim {A = λ bot → suc m ≡ 0} (gcd[m,n]≢0 (suc m) n (inl snotz) gmn) | ||
|
|
||
| gcd[m,n]≡0⇒n≡0 : ∀ {m n} → gcd m n ≡ 0 → n ≡ 0 | ||
| gcd[m,n]≡0⇒n≡0 {m}{n} gmn = gcd[m,n]≡0⇒m≡0 {n}{m} |
There was a problem hiding this comment.
transporting on cong (λ a → a ≡ 0) is the same as composing with the reverse path. In my opinion, it would be better to write gcd[m,n]≡0⇒m≡0 {n} {m} (gcdSym n m ∙ gmn), avoiding unnecessary transports.
More generally, I see you are using multiple times the pattern transport + cong, where you could have used subst instead.
However, I'm not a maintainer; I just noticed a couple of places where the code could be made shorter. Feel free to ignore these comments if not relevant
There was a problem hiding this comment.
Thanks. I'll look at this shortly.
3 participants
No description provided.