Nat (cooltt.Core.Refiner.Nat)

val formation : Tactic.Tp.tac

val literal : int -> Tactic.Chk.tac

val suc : Tactic.Chk.tac -> Tactic.Chk.tac

val elim : 
  Tactic.Chk.tac ->
  Tactic.Chk.tac ->
  Tactic.Chk.tac ->
  Tactic.Syn.tac ->
  Tactic.Syn.tac