mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
[ minor ] Make NotBothZero
parameter of standard gcd
to be erased
This commit is contained in:
parent
8d7b993cca
commit
ff6afb0c59
@ -390,7 +390,7 @@ Integral Nat where
|
||||
|
||||
export
|
||||
covering
|
||||
gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
|
||||
gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
|
||||
gcd a Z = a
|
||||
gcd Z b = b
|
||||
gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNonZero)
|
||||
|
Loading…
Reference in New Issue
Block a user