Struct WhereClause 

pub struct WhereClause {
    pub name: String,
    pub params: Vec<Binder>,
    pub ty: Option<Located<SurfaceExpr>>,
    pub val: Located<SurfaceExpr>,
}

A where clause for local definitions attached to a definition or theorem.

Example:

def foo (n : Nat) : Nat := bar n + baz n where
  bar (x : Nat) : Nat := x + 1
  baz (x : Nat) : Nat := x * 2

Fields

name: String

Name of the local definition.

params: Vec<Binder>

Parameters of the local definition.

ty: Option<Located<SurfaceExpr>>

Optional type annotation.

val: Located<SurfaceExpr>

Value (body) of the local definition.

Implementations

impl WhereClause

pub fn new( name: String, params: Vec<Binder>, ty: Option<Located<SurfaceExpr>>, val: Located<SurfaceExpr>, ) -> Self

Create a new where clause.

Trait Implementations

impl Clone for WhereClause

fn clone(&self) -> WhereClause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WhereClause

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

Formats the value using the given formatter.

impl Display for WhereClause

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

Formats the value using the given formatter.

impl PartialEq for WhereClause

fn eq(&self, other: &WhereClause) -> 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 StructuralPartialEq for WhereClause