Struct TypeClass 

pub struct TypeClass {
    pub name: Name,
    pub params: Vec<Name>,
    pub ty: Expr,
    pub methods: Vec<Method>,
    pub super_classes: Vec<Name>,
    pub is_prop: bool,
}

A type class declaration.

For example, class Add (α : Type) declares a type class named Add with one type parameter and one method add : α → α → α.

Fields

name: Name

Name of the class (e.g., Add, Mul, Inhabited).

params: Vec<Name>

Names of the type parameters.

ty: Expr

The full type of the class (as a Pi-type).

methods: Vec<Method>

Methods declared in the class, in declaration order.

super_classes: Vec<Name>

Names of super-classes that instances must also implement.

is_prop: bool

Whether this class is in Prop (proof-irrelevant).

Implementations

impl TypeClass

pub fn new(name: Name, params: Vec<Name>, ty: Expr) -> Self

Create a new type class with no methods or super-classes.

pub fn add_method(&mut self, method: Method)

Add a method to the class.

pub fn add_super(&mut self, super_name: Name)

Add a super-class dependency.

pub fn mark_prop(self) -> Self

Mark this class as living in Prop.

pub fn find_method(&self, name: &Name) -> Option<&Method>

Look up a method by name.

pub fn has_super(&self, name: &Name) -> bool

Check whether the class has a super-class with the given name.

pub fn method_count(&self) -> usize

Count methods in the class.

pub fn is_empty(&self) -> bool

Check whether the class has any methods.

pub fn method_names(&self) -> impl Iterator<Item = &Name>

Iterate over all method names.

pub fn has_super_classes(&self) -> bool

Check whether the class has any super-classes.

pub fn arity(&self) -> usize

Number of type parameters.

Trait Implementations

impl Clone for TypeClass

fn clone(&self) -> TypeClass

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TypeClass

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

Formats the value using the given formatter.