Struct nar::syntax::common::ConHead

pub struct ConHead {
    pub name: Ident,
    pub cons_ix: GI,
    pub ductive: Ductive,
    pub fields: Vec<String>,
}

Constructor information. Agda.

Fields

name: Ident

Constructor name.

cons_ix: GI

Index of the constructor.

ductive: Ductive

Records might be coinductive.

fields: Vec<String>

Field names. This allows us to project fields from a record without the TCS.

Methods

impl ConHead

pub fn pseudo(name: Ident) -> Self

pub fn new(name: Ident, ix: GI, ductive: Ductive, fields: Vec<String>) -> Self

Trait Implementations

impl Clone for ConHead

fn clone(&self) -> ConHead

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ConHead

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

Formats the value using the given formatter.

impl Display for ConHead

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

Formats the value using the given formatter.

impl Eq for ConHead

impl PartialEq<ConHead> for ConHead

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl StructuralEq for ConHead

impl StructuralPartialEq for ConHead