Make `cong` more flexible.

See merge request !20

Minor changes in rule distinct_elim, nary_elim, distinct_elim, and source code docu. in doc.tex

See merge request !18

Add shuffle rule

See merge request !17

Fix typos

See merge request !16

Positional arguments start at 0.

See merge request !15

Add bind_let rule

See merge request !14

Hans-Jörg authored 8 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>