Tactics (cooltt.Frontend.Tactics)

module D := Core.CodeUnit.Domain

module S := Core.CodeUnit.Syntax

module RM := Core.Monads.RefineM

module CS := ConcreteSyntax

module R := Core.Refiner

val is_total : D.tele -> [ `TotalAll | `TotalSome | `NotTotal ] RM.m

Determines whether a signature is: `TotalAll : A total space created by the `total` tactic, where all fields but `fib` are patched `TotalSome : A total space created by the `total` tactic, where at least one non-`fib` field is *not* patched `NotTotal : Not a total space created by the `total` tactic

val intro_subtypes_and_total : Core.Tactic.Chk.tac -> Core.Tactic.Chk.tac

val intro_implicit_connectives : Core.Tactic.Chk.tac -> Core.Tactic.Chk.tac

val elim_implicit_connectives : Core.Tactic.Syn.tac -> Core.Tactic.Syn.tac

val elim_implicit_connectives_and_total : 
  Core.Tactic.Syn.tac ->
  Core.Tactic.Syn.tac

val intro_conversions : Core.Tactic.Syn.tac -> Core.Tactic.Chk.tac

val open_ : 
  Core.Tactic.Syn.tac ->
  (Core.Ident.t -> Core.Ident.t option) ->
  (Core.Tactic.var list -> Core.Tactic.Chk.tac) ->
  Core.Tactic.Chk.tac

Brings all fields of a struct into scope, potentially applying a renaming.

val open_syn : 
  Core.Tactic.Syn.tac ->
  (Core.Ident.t -> Core.Ident.t option) ->
  (Core.Tactic.var list -> Core.Tactic.Syn.tac) ->
  Core.Tactic.Syn.tac

Brings all fields of a struct into scope, potentially applying a renaming.

val tele_of_sign : Core.Tactic.Tp.tac -> Core.Tactic.Tele.tac

Attempt to extract a telescope from a signature.

val kan_tele_of_sign : Core.Tactic.Chk.tac -> Core.Tactic.KanTele.tac

Attempt to extract a kan telescope from a signature code.

val tac_nary_quantifier : 
  ('a, 'b) R.quantifier ->
  (Core.Ident.t * 'a) list ->
  'b ->
  'b

val match_goal : 
  ((D.tp * D.cof * D.tm_clo) -> Core.Tactic.Chk.tac RM.m) ->
  Core.Tactic.Chk.tac

val refine : 
  ((D.tp * D.cof * D.tm_clo) list -> exn option -> Core.Tactic.Chk.tac) ->
  Core.Tactic.Chk.tac

module Elim : sig ... end

module Equations : sig ... end