Core.Refiner
This is the basis of trusted inference rules for cooltt. This module also contains some auxiliary tactics, but these don't need to be trusted so they should be moved elsewhere.
module D := CodeUnit.Domain
module S := CodeUnit.Syntax
module RM := Monads.RefineM
type ('a, 'b) quantifier = 'a -> (Ident.t * (Tactic.var -> 'b)) -> 'b
module Hole : sig ... end
module Probe : sig ... end
module Dim : sig ... end
module Cof : sig ... end
module Prf : sig ... end
module Univ : sig ... end
module El : sig ... end
module ElV : sig ... end
module ElHCom : sig ... end
module Pi : sig ... end
module Sg : sig ... end
module Telescope : sig ... end
module KanTelescope : sig ... end
module Signature : sig ... end
module Sub : sig ... end
module Nat : sig ... end
module Circle : sig ... end
module Structural : sig ... end