Examine interplay between type inference and term quotations.

[phlegmaticprogrammer]

If a term literal contains a quoted term, then it seems that the type of that term should be used during type inference for the term literal. Is this the case already? If not, find out if it is feasible to implement this behaviour and implement it if it is.

[phlegmaticprogrammer]

As a motivation for why this behaviour seems desirable: Imagine you have for example a pattern match

match t
  case '∀ x. ‹u› x x' =>
    let 'x = 3'
    theorem '‹u› x x' 
      apply(t, 'x')

Then in the second appearance of '‹u› x x' the type inference needs to take the known type of u into account, otherwise the type inference might not yield the intended type. Note that "theorem" is not part of ProofScript yet, but it should be added.

[phlegmaticprogrammer]

As for properties of pattern matching, what you would also want is the following:

match t
  case term-literal =>
    theorem ' ‹term-literal› = ‹term-literal› ' 
      reflexive t

If the case branch matches, then it should yield a valid theorem.

[phlegmaticprogrammer]

That seems to all work out fine.