Skip to content

Abstraction

Viktor Kuncak requested to merge github/fork/SimonGuilloud/abstraction into main

Created by: SimonGuilloud

Abstract the identifiers in kernel's labels. Indices are treated as integers, faster generation.

Printer and Parser now don't remove single-arity disjunction and cunjunction (tactics and everything can behave differently on either versions even if they are OCBSL equivalent, also debugging).

Unused front parts have been removed and are in a separate branch. It was confusing for LISA user and increase codebase to be maintained.

Merge request reports