Closed olaure01 closed 3 years ago
In order to define an auto-reverse mode, or to run a full reversible phase on a double click on a negative connective, function invertible_proof_part applies all possible reversible rules bottom-up to a given sequent.
invertible_proof_part
In order to define an auto-reverse mode, or to run a full reversible phase on a double click on a negative connective, function
invertible_proof_partapplies all possible reversible rules bottom-up to a given sequent.