wip: check for beta-equiv during type checking

[NeuralCoder3]

Is an explicit beta equivalence check and mode needed? Shouldn't it be enough to eagerly evaluate every function on the type level as if the filter was true?

[leissa]

Is an explicit beta equivalence check and mode needed? Shouldn't it be enough to eagerly evaluate every function on the type level as if the filter was true?

We are already doing this. Problem is, if you have a type like this: «pow (2, 3), .Nat». Just by looking at pow (2, 3) you have no idea that it occurs within a type. I also thought to add the evaluation directly to the constructors of the type formations ([ ... ], «...», etc) but check out my comments in Discord, too.

[leissa]

hopefully superseded by #229.