idris-0.11.1: test/interactive013/interactive013.idr

gcd : (x : Nat) -> (y : Nat) -> CmpNat x y -> Nat
gcd aa bb cc = ?gcd_rhs