Typing (gillian.Engine.Typing)

val type_lexpr : 
  Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Type.t option * bool

Given a typing environment and an expressions, returns a triple containing:

A type if we found a necessary type
A boolean: true if the expression is typable, false if is definitely a type error
A list of corrections missing (not sure about that one ?)

val infer_types_expr : Symbolic.Type_env.t -> Gillian.Gil_syntax.Expr.t -> unit

val infer_types_formula : 
  Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Formula.t ->
  unit

val reverse_type_lexpr : 
  bool ->
  Symbolic.Type_env.t ->
  (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list ->
  Symbolic.Type_env.t option

val te_of_list : 
  (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list ->
  Symbolic.Type_env.t option

val naively_infer_type_information : 
  Symbolic.Pure_context.t ->
  Symbolic.Type_env.t ->
  unit

val substitution_in_place : 
  Gillian.Symbolic.Subst.t ->
  Symbolic.Type_env.t ->
  unit