Structural (cooltt.Core.Refiner.Structural)

val let_ : 
  ?ident:Ident.t ->
  Tactic.Syn.tac ->
  (Tactic.var -> Tactic.Chk.tac) ->
  Tactic.Chk.tac

val let_syn : 
  ?ident:Ident.t ->
  Tactic.Syn.tac ->
  (Tactic.var -> Tactic.Syn.tac) ->
  Tactic.Syn.tac

val lookup_var : Ident.t -> Tactic.Syn.tac

val level : int -> Tactic.Syn.tac

val generalize : Ident.t -> Tactic.Chk.tac -> Tactic.Chk.tac

val unfold : Ident.t list -> Tactic.Chk.tac -> Tactic.Chk.tac

val abstract : name:Ident.t option -> Tactic.Chk.tac -> Tactic.Chk.tac