Struct Lhs 

pub(super) struct Lhs {
    pub(super) tele: Tele,
    pub(super) has_absurd: bool,
    pub(super) pats: Vec<CoreCopat>,
    pub(super) ty: Term,
    pub(super) pat_sub: Rc<Subst>,
    pub(super) as_binds: Vec<AsBind>,
}

Result of checking the LHS of a clause. Agda.

Fields

tele: Tele

$\Delta$: The types of the pattern variables, in internal dependency order. Corresponds to clauseTel (in Agda).

has_absurd: bool

Whether the LHS has at least one absurd pattern.

pats: Vec<CoreCopat>

The patterns in internal syntax.

ty: Term

The type of the body. Is $b~\sigma$ if $\Gamma$ is defined.

pat_sub: Rc<Subst>

Substitution version of pats, only up to the first projection pattern. $\Delta \vdash \text{pat_subst} : \Gamma$. Where $\Gamma$ is the argument telescope of the function. This is used to update inherited dot patterns in with-function clauses.

as_binds: Vec<AsBind>

As-bindings from the left-hand side. Return instead of bound since we want them in where’s and right-hand sides, but not in with-clauses

Trait Implementations

impl Clone for Lhs

fn clone(&self) -> Lhs

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.