mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 12:14:26 +03:00
498421a236
This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too.
18 lines
243 B
Idris
18 lines
243 B
Idris
%default partial
|
|
|
|
foo : (Nat, Nat) -> Nat
|
|
foo (Z, Z) = Z
|
|
|
|
bar : {a : _} -> a -> Nat
|
|
bar Z = Z
|
|
bar (S _) = S Z
|
|
|
|
cty : (a : Type) -> a -> Nat
|
|
cty Nat Z = Z
|
|
cty Nat (S _) = S Z
|
|
cty _ x = S (S Z)
|
|
|
|
badBar : a -> Nat
|
|
badBar Z = Z
|
|
badBar (S _) = S Z
|