meta-logic / sellf

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

Built-in kinds #9

Open gisellemnr opened 7 years ago

gisellemnr commented 7 years ago

As of now, we have the following built-in kinds: term, form and world for sequent systems' specifications. Think if it is not better to have the user declare those pro-actively.