ScopedTerm (elpi.Elpi_compiler.Compiler

module SimpleTerm : sig ... end

type 'scope const = {

scope : 'scope;
name : F.t;
ty : TypeAssignment.t MutableOnce.t;
loc : Elpi_util.Util.Loc.t;

}

val pp_const : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'scope const ->
  Ppx_deriving_runtime.unit

val show_const : 
  'scope. (Ppx_deriving_runtime.Format.formatter ->
            'scope ->
            Ppx_deriving_runtime.unit) ->
  'scope const ->
  Ppx_deriving_runtime.string

val mk_const : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  scope:'a ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  'a const

val mk_bound_const : 
  ?ty:TypeAssignment.t MutableOnce.t ->
  lang:Scope.language ->
  F.t ->
  loc:Elpi_util.Util.Loc.t ->
  Scope.t const

val bind_const : string const -> Scope.t const

val mk_global_const : name:F.t -> loc:Elpi_util.Util.Loc.t -> Scope.t const

val const_of_symb : 
  types:TypingEnv.t ->
  Symbol.t ->
  loc:Elpi_util.Util.Loc.t ->
  Scope.t const

val clone_const : ?clone_scope:('a -> 'a) -> 'a const -> 'a const

type spill_info =

| NoInfo
| Main of int
| Phantom of int

val pp_spill_info : 
  Ppx_deriving_runtime.Format.formatter ->
  spill_info ->
  Ppx_deriving_runtime.unit

val show_spill_info : spill_info -> Ppx_deriving_runtime.string

type t_ =

| Impl of SimpleTerm.impl_kind * Elpi_util.Util.Loc.t * t * t
| Discard
| Var of Scope.t const * t list
| App of Scope.t const * t list
| Lam of Scope.language const option * ScopedTypeExpression.e option * t
| CData of Elpi_util.Util.CData.t
| Spill of t * spill_info Stdlib.ref
| Cast of t * ScopedTypeExpression.e

and t = {

}

val pp_t_ : 
  Ppx_deriving_runtime.Format.formatter ->
  t_ ->
  Ppx_deriving_runtime.unit

val show_t_ : t_ -> Ppx_deriving_runtime.string

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

val type_of : t -> TypeAssignment.ty

val lam : int

val app : int

val lvl_of : t_ -> int

val get_lam_name : (F.t * 'a) option -> F.t

val mk_empty_lam_type : 
  (F.t * Elpi_util.Util.Loc.t * 'a) option ->
  'a const option

val build_infix_constant : Scope.t const -> Elpi_util.Util.Loc.t -> t

val is_infix_constant : F.t -> bool

val intersperse : (Elpi_util.Util.Loc.t -> t) -> t list -> t list

val pretty_lam : 
  Stdlib.Format.formatter ->
  Scope.language const option ->
  ScopedTypeExpression.e option ->
  t ->
  unit

val pretty : Stdlib.Format.formatter -> t -> unit

val pretty_ : Stdlib.Format.formatter -> t_ -> unit

val pretty_parens : lvl:int -> Stdlib.Format.formatter -> t -> unit

val pretty_parens_lam : lvl:int -> Stdlib.Format.formatter -> t -> unit

val equal : TypingEnv.t -> ?types:bool -> t -> t -> bool

val compare : 'a -> 'b -> 'c

val in_scoped_term : t -> Elpi_util.Util.CData.t

val out_scoped_term : Elpi_util.Util.CData.t -> t

val is_scoped_term : Elpi_util.Util.CData.t -> bool

val of_simple_term : loc:Elpi_util.Util.Loc.t -> SimpleTerm.t_ -> t_

val of_simple_term_loc : SimpleTerm.t -> t

val unlock : t -> t_

val fresh : unit -> F.t

val rename : Scope.language -> F.t -> F.t -> t_ -> t_

val rename_loc : Scope.language -> F.t -> F.t -> t -> t

val clone_loc : loc:Elpi_util.Util.Loc.t -> t -> t

val clone : loc:Elpi_util.Util.Loc.t -> t_ -> t_

val beta : t -> t list -> t_

module QTerm : sig ... end

val is_var : t_ -> bool