search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

Termination checker doesn't check args not being matched on #93

Closed florence closed 4 years ago

florence commented 5 years ago

See

##lang cur
(require
  cur/stdlib/nat
  cur/stdlib/equality
  cur/stdlib/sugar)

(define/rec/match bang!1 : [n : Nat] -> (== 0 1)
 [=> (bang!1 n)])

(define/rec/match bang!2 : -> (== 0 1)
 [=> (bang!2)])

bang!1 infinite loops.

using bang!2 in the gives:

identifier used out of context: #<syntax:cur.rkt:11:6 bang!2>
florence commented 5 years ago

Actually this might just be that it accepts programs where the argument size doesn't decrease. See:

#lang cur
(require
  cur/stdlib/nat
  cur/stdlib/equality
  cur/stdlib/sugar)

(define/rec/match bang! : Nat -> (== 0 1)
 [n => (bang! n)])

Which typechecks.