search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

Wrong evaluation order with sequential modifier #1033

Closed NotBad4U closed 5 months ago

NotBad4U commented 5 months ago

Hi everyone!

When the modifier sequential is used on a symbol, the order of execution is reversed. The last case is evaluated first ("toto (⊤ ∧ ⊤) ↪ ⊥" in the below example).

sequential symbol toto: Prop →  Prop;
rule toto (⊤ ∧ ⊤) ↪ ⊤
with toto (⊤ ∧ ⊤) ↪ ⊥;

compute toto (⊤ ∧ ⊤);   // compute ⊥
fblanqui commented 5 months ago

Hi @gabrielhdt . This is for you I think. ;-) I guess there is a list to reverse somewhere...