Type inference for LCNF #

@[inline, reducible]

We use a regular local context to store temporary local declarations created during type inference.

Instances For

    Return true if type should be erased. See item 1 in the note above where x ◾ ◾ is a proposition and should be erased when the universe level parameter is set to 0.

    Remark: predVars is a bitmask that indicates whether de-bruijn variables are predicates or not. That is, #i is a predicate if predVars[predVars.size - i - 1] = true

    Instances For

      Return true if the given LCNF are equivalent. List Nat and (fun x => List x) Nat are both equivalent.