package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type term = private
| Kind
| Type of Basic.loc
| DB of Basic.loc * Basic.ident * int
| Const of Basic.loc * Basic.name
| App of term * term * term list
| Lam of Basic.loc * Basic.ident * term option * term
| Pi of Basic.loc * Basic.ident * term * term
val pp_term : term Basic.printer
val mk_Kind : term
val mk_DB : Basic.loc -> Basic.ident -> int -> term
val mk_Const : Basic.loc -> Basic.name -> term
val mk_Lam : Basic.loc -> Basic.ident -> term option -> term -> term
val mk_Pi : Basic.loc -> Basic.ident -> term -> term -> term
type untyped_context = (Basic.loc * Basic.ident) list
type typed_context = (Basic.loc * Basic.ident * term) list
val rename_vars_with_typed_context : typed_context -> term -> term
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>