package alba
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=062f33c55ef39706c4290dff67d5a00bf009051fd757f9352be527f629ae21fc
md5=eb4edc4d6b7e15b83d6397bd34994153
doc/alba.core/Alba_core/Gamma_algo/Make/index.html
Module Gamma_algo.MakeSource
Parameters
Signature
type_of_term term gamma
Compute the type of term
Precondition: term must be welltyped and the context valid.
val split_kind :
Term.typ ->
Gamma.t ->
((Term.Pi_info.t * Term.typ) list * Term.Sort.t) optionsplit_kind k gamma:
Compute the arguments and the sort of the kind k. If typ does not reduce to a kind, then return None.
Precondition: k must be welltyped and the context gamma must be valid.
A kind has the form
all (x: A) (y: B) .... : swhere s is a sort.
sort_of_kind typ gamma
Compute the sort of the kind typ. If typ does not reduce to a kind, then return None.
Precondition: typ must be welltyped and the context gamma must be valid.
A kind has the form
all (x: A) (y: B) .... : swhere s is a sort.
is_kind typ gamma
Is the welltyped term typ in the valid context gamma a kind?
keynormal term gamma
Compute the key normal form of the welltyped term term in the valid context gamma.
normalize_pi typ gamma
Precondition:
typ must be a valid type
Result: typ is expanded until the form
all (a: A) (b: B) ... : Ris reached where R cannot be expanded further into a product type.
normalize term gamma
Compute the normal form of the welltyped term term in the valid context gamma.