Hans-Jörg authored 8 months ago and Hans-Jörg committed 8 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.

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".

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

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

Hans-Jörg authored 11 months ago and Lachnitt committed 11 months ago

Co-authored-by: Hans-Jörg <commits@schurr.at>

Addresses #37

Adresses #35

Addresses #36

This follows the advice given here:
https://latex.org/forum/viewtopic.php?t=32205
The option changes how destination names are defined.

Also fixes two other small typos related to references.

Should address:
#39

Addresses #40

- adress normalizing of terms with context push (and other typos)
- Remark on missing Gamma

- replace semantic by semantics
- apply some review suggestions

The simplification `(P -> Q) -> Q => P or Q` is already covered
by `bool_simplify`.