package alba

  1. Overview
  2. Docs
Alba compiler

Install 

dune-project
 Dependency

albatross-lang.sourceforge.net Readme Edit opam file Versions (5)

Authors

  1. H
    Helmut Brandl <helmut.brandl@gmx.net>

Maintainers

  1. H
    Helmut Brandl <helmut.brandl@gmx.net>

Sources

0.4.1.tar.gz
sha256=439b1dce07c86e914d1ebf1712c5581418314b0c8d13594f27a698b1d25fe272
md5=5cf58d4ed4eacbe6f330e9d2378ef5c6

doc/alba.albalib/Albalib/Gamma_algo/Make/index.html

Module Gamma_algo.MakeSource

Parameters

module Gamma : GAMMA

Signature

Sourceval type_of_term : Term.t -> Gamma.t -> Term.typ

type_of_term term gamma

Compute the type of term

Precondition: term must be welltyped and the context valid.

Sourceval sort_of_kind : Term.typ -> Gamma.t -> Term.Sort.t option

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) .... : s

where s is a sort.

Sourceval is_kind : Term.typ -> Gamma.t -> bool

is_kind typ gamma

Is the welltyped term typ in the valid context gamma a kind?

Sourceval key_normal : Term.t -> Gamma.t -> Term.t

keynormal term gamma

Compute the key normal form of the welltyped term term in the valid context gamma.