feat: Tagged InferenceSystem

[fmontesi]

Adds a tagged version of InferenceSystem, so that multiple inference systems for the same type can be instantiated and distinguished by means of a tag. Usage is exemplified with the multiplicative fragment of classical linear logic.

[thomaskwaring]

is there a reason this isn't S : Type*

[fmontesi]

That's what it was originally, but it gave me type errors, I don't clearly remember where (maybe DerivationsIn).

[thomaskwaring]

okay, it does seem very restrictive to have it Type 0 — can you fix it with explicit universes?

[fmontesi]

Oh, actually, I tried again and it worked now. It must've been something weird with a previous version.

Thanks for catching this.

[chenson2018]

Just a few style questions/suggestions.

[chenson2018]

It took me a moment to understand why this was an empty inductive. I feel like I have more often seen something like

def InferenceSystem.Default := Unit

in these situations. I think this is functionally identical, but maybe easier to understand the intent for the next person like me who was confused.

[fmontesi]

My purpose was to do the simplest possible thing, which is an empty type.

What's the point of making Default inhabited?

[chenson2018]

It doesn't matter that it's inhabited, you could use Empty just as easily. My point is that it doesn't really matter: we could pick any existing type and say that by convention this represents the default.

So I'd personally find def InferenceSystem.Default := Empty the more readable exact equivalent I suppose. Maybe a short comment is warranted in either case.

[chenson2018]

Approving, as my last comment about InferenceSystem.Default seems fine either way, maybe a matter of personal taste.

[chenson2018]

(I removed from the auto merge so you can decide what you prefer writing, and maybe leave a comment.)

[fmontesi]

Thanks. I've made it an opaque alias for Empty, which should be equivalent to my original.