Macro term 

macro_rules! term {
    ($(#[$fn_attrs:meta])* $fn_vis:vis fn $fn:ident $($rest:tt)*) => { ... };
    ($(#[$fn_attrs:meta])* $fn_vis:vis const fn $fn:ident $($rest:tt)*) => { ... };
}

Define a term, consisting of:

• A non-instantiable struct type $name implementing the Term trait
• A constructor function with the same name that creates a Value<$name>
• A $name::eq function that construct a ValueEq from ValueEqs for each term parameter

SAFETY: must ensure that, for any given input terms, and for equal values, the values returned are all equal

Example

fn-like syntax:

deptypes::term! {
    pub fn Add(a, b) -> unsafe <a::Type as core::ops::Add<b::Type>>::Output
        where a::Type: core::ops::Add<b::Type> {
        core::ops::Add::add(a, b)
    }
}

Code generated by the macro

use core::marker::PhantomData;
use deptypes::term::{Term, Value, ValueEq};
 
#[allow(non_camel_case_types)]
pub struct Add<a: Term, b: Term> {_marker: (PhantomData<fn() -> Value<a>>, PhantomData<fn() -> Value<b>>)}
 
#[allow(non_camel_case_types)]
impl<a: Term, b: Term> Term for Add<a, b>
    where a::Type: core::ops::Add<b::Type> {
    type Type = <a::Type as core::ops::Add<b::Type>>::Output;
}
 
#[allow(non_snake_case)]
#[allow(non_camel_case_types)]
pub fn Add<a: Term, b: Term>(a: Value<a>, b: Value<b>) -> Value<Add<a, b>>
    where a::Type: core::ops::Add<b::Type> {
    let (a, b) = (a.into_inner(), b.into_inner());
    let ret = {core::ops::Add::add(a, b)};
    unsafe {Value::definition(ret, &Add {_marker: (PhantomData, PhantomData)})}
}
 
#[allow(non_camel_case_types)]
impl<a0: Term, b0: Term> Add<a0, b0> {
    pub fn eq<a1: Term, b1: Term>(_: ValueEq<a0, a1>, _: ValueEq<b0, b1>)
     -> ValueEq<Self, Add<a1, b1>> {
        unsafe { ValueEq::axiom() }
    }
}