search

gmalecha / mirror-core

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

boolean equality for expr? #61

Closed jldodds closed 9 years ago

jldodds commented 9 years ago

Is there a semi-decidable equality function for exprs that assums the two exprs are in the same context?

gmalecha commented 9 years ago

There is a RelDec instance for [expr] given [RelDec] instances for [typ] and [sym].

See https://github.com/gmalecha/mirror-core/blob/master/theories/Lambda/ExprCore.v#L104

(reopen if this isn't what you're looking for)