search

gmalecha / mirror-core

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

New lemma #60

Closed jldodds closed 9 years ago

jldodds commented 9 years ago

Is the following true?

typeof_expr tus tvs e = Some t -> exists val, exprD' tus tvs t e = Some val

If so I think it might be useful

jldodds commented 9 years ago

@jesper-bengtson just pointed me to ExprFacts.exprD'_typeof_expr which is just what I need

gmalecha commented 9 years ago

Yup.