search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Sanity check values when they pass through [id] #58

Closed gmalecha closed 9 years ago

gmalecha commented 9 years ago

id can produce ill-typed terms, e.g.

Reify Pattern patterns += (@RGet 0 RIgnore) => (fun (n : id nat) => @Inj typ func (N n)).

reify (fun x : nat => x).

will try to construct (Abs tyNat (Inj x)) even though x is not bound anywhere.