Tactic.Tp
include Tactic
type tac
val update_span : Basis.LexingUtil.span option -> tac -> tac
val whnf : tac -> tac
val rule : ?name:string -> S.tp RM.m -> tac
val virtual_rule : ?name:string -> S.tp RM.m -> tac
A "virtual type" is one that is only permitted to appear as the domain of a pi type
val run : tac -> S.tp RM.m
Only succeeds for non-virtual types
val run_virtual : tac -> S.tp RM.m
Virtual types allowed
val map : (S.tp RM.m -> S.tp RM.m) -> tac -> tac