Closed wilbowma closed 6 years ago
This type checks
#lang cur (require cur/stdlib/prop cur/stdlib/sugar cur/stdlib/nat cur/stdlib/bool) (:: (λ [n : Nat] (match n #:return (== Bool (nat-equal? (plus 1 n) 0) false) [z (refl Bool false)] [(s n-1) (refl Bool false)])) (Π [n : Nat] (== Bool (nat-equal? (plus 1 n) 0) false)))
but this one does not:
;; use n+1 instead of 1+n (:: (λ [n : Nat] (match n #:return (== Bool (nat-equal? (plus n 1) 0) false) [z (refl Bool false)] [(s n-1) (refl Bool false)])) (Π [n : Nat] (== Bool (nat-equal? (plus n 1) 0) false)))
In the branches, we also know the value of n, so it ought to be able to reduce plus at least 1 step, but for some reason, this doesn't happen.
Match is dead; long live match. #55
This type checks
but this one does not:
In the branches, we also know the value of n, so it ought to be able to reduce plus at least 1 step, but for some reason, this doesn't happen.