Hole Type Inference

Annotate each .Hole node with a type inferred from its surrounding context using the SemanticModel and computeExprType. After this pass every Hole carries some ty so that the hole elimination pass can generate correctly typed uninterpreted functions.

structure Strata.Laurel.InferHoleState : Type

• model : SemanticModel
• currentOutputType : HighTypeMd

def Strata.Laurel.inferHoleTypes (model : SemanticModel) (program : Program) : Program

Annotate every .Hole in the program with a type inferred from context.

Equations

• One or more equations did not get rendered due to their size.