Struct Signature 

pub struct Signature { /* private fields */ }

What a settled constant’s type says about its applications, at one universe instantiation.

The type’s telescope Π (x₀ : A₀) … (xₙ₋₁ : Aₙ₋₁), B, walked once under fresh variables, gives the universe uᵢ of every binder type and v of the result. Universes do not depend on terms, so these are the universes of every application’s parts too: an argument at position i is a proof exactly when uᵢ is zero, and an application to k ≤ n arguments, whose type is Π (xₖ : Aₖ) … , B, lives in imax(uₖ, … imax(uₙ₋₁, v)) — zero exactly when v is. So whether an application is a proof is read off its head and its argument count, without inferring a type. Past the telescope — a result type that becomes a Π only once arguments are substituted — nothing is known.

Implementations

impl Signature

pub fn proof_args(&self) -> u64

The argument positions (below MAX_TRACKED) whose binder type is a proposition.

pub fn is_proof(&self, k: usize) -> Option<bool>

Whether an application to k arguments is a proof, if the telescope says.

pub fn is_proposition(&self, k: usize) -> Option<bool>

Whether an application to k arguments is a proposition, if the telescope says: only a full application whose result is a sort is a type at all.

Trait Implementations

impl Clone for Signature

fn clone(&self) -> Signature

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Signature

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Signature

fn default() -> Signature

Returns the “default value” for a type.

impl PartialEq for Signature

fn eq(&self, other: &Signature) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for Signature

impl Eq for Signature

impl StructuralPartialEq for Signature