pub struct Clause {
pub pat_tele: Tele,
pub patterns: Vec<CoreCopat>,
pub body: Option<Term>,
}
Expand description
Function clauses. Agda.
Fields§
§pat_tele: Tele
$\Delta$. The types of the pattern variables in dependency order.
patterns: Vec<CoreCopat>
$\Delta \vdash ps$. The de Bruijn indices refer to $\Delta$.
body: Option<Term>
Some(v)
if $\Delta \vdash v$, while None
if the patterns are absurd.
Implementations§
Trait Implementations§
impl Eq for Clause
impl StructuralPartialEq for Clause
Auto Trait Implementations§
impl Freeze for Clause
impl RefUnwindSafe for Clause
impl Send for Clause
impl Sync for Clause
impl Unpin for Clause
impl UnwindSafe for Clause
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more