Module Frontend.Tactics

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

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

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

Attempt to extract a telescope from a signature.

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 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