Skip to content

Adding eq_symmetric rule

Haniel Barbosa requested to merge devel/add-elab-rules into master

This adds a new rule used to elaborate implicity reasoning with equality symmetry. This addresses issue #43 (closed).

Merge request reports