Add bind_let rule

See merge request !14

Hans-Jörg authored 7 months ago and Hans-Jörg committed 7 months ago

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

This rule is used by Carcara's elaborator when eliminating the
implicit use of symmetry of equality.

Make the description of the comp_simplify rule clearer

See merge request !13

This addresses
#44

By changing the variable names we clarify that those are rules
that can match.

Furthermore, we also change all occurrences of the very awkward
"as long as possible" to "until a fixed point is reached".

Add weakening rule

See merge request !11

Fix potential typo in hole rule?

See merge request !10

Document cvc5-style numerals

See merge request !5

Haniel Barbosa authored 10 months ago and Hans-Jörg committed 8 months ago

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Add index to four rules

Closes #34

See merge request !9

Adding eq_symmetric rule

See merge request !8

Update forall_inst

See merge request !7

Haniel Barbosa authored 10 months ago and Hans-Jörg committed 10 months ago

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Add la_mult_pos and la_mult_neg rules

See merge request !6

Haniel Barbosa authored 10 months ago and Lachnitt committed 10 months ago

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>