Tactic.KanTele
include Tactic
type tac
val update_span : Basis.LexingUtil.span option -> tac -> tac
val whnf : tac -> tac
val rule : ?name:string -> (D.tp -> S.kan_tele RM.m) -> tac
val run : tac -> D.tp -> S.kan_tele RM.m