on master help sign in
Idris-dev/test/interactive013/interactive013.idr
4 lines 76 B history raw
2gcd : (x : Nat) -> (y : Nat) -> CmpNat x y -> Nat
3gcd aa bb cc = ?gcd_rhs