search

meta-logic / sellf

SubExponential Linear Logic Framework for reasoning about sequent calculus systems
7 stars 2 forks source link

Functional code #13

Closed gisellemnr closed 6 years ago

gisellemnr commented 6 years ago

Some methods (cutcoherent and the like) are not implemented in a pure functional way, using mutable variables for some tasks. Rewrite them functionally.

gisellemnr commented 6 years ago

Also check_principalcut and check_atomicelim in sellf.ml