Type Definition kontroli::arc::Typing

type Typing<'s> = Typing<RTerm<'s>>;

Implementations

impl<'s> Typing<'s>

pub fn declare(
    typ: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn define(
    oty: Option<RTerm<'s>>,
    term: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn check(self, sig: &Signature<'s>) -> Result<Self, Error>

Verify whether t: A if this was not previously checked.

Return a typing registering that t: A has been checked.

pub fn new(it: Intro<'s>, sig: &Signature<'s>) -> Result<Self, Error>

Construct a typing from an introduction command.

An introduction command can have many shapes, such as x: A, x := t, x: A := t, ... The type A of the newly introduced symbol is (a) inferred from its defining term t if not given and (b) verified to be of a proper sort. In case a defining term t is given, t is registered, along with the information whether the type A was inferred from it.

Constructing a typing from a command of the shape x: A := t does not check whether t: A. For this, the check function can be used. This allows us to postpone and parallelise type checking.