Trait LeanArgs 

pub trait LeanArgs<'lean>: Sized + SealedArgs {
    const ARITY: usize;
}

Per-arity marker for LeanExported’s argument tuple.

Sealed via SealedArgs; downstream cannot implement it. Macro-stamped for arity-0..=12 tuples whose elements implement LeanAbi. Used at lookup time to reject ARITY > 0 against a Lean nullary-constant global.

Required Associated Constants

const ARITY: usize

Number of arguments the tuple represents.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<'lean> LeanArgs<'lean> for ()

const ARITY: usize = 0

impl<'lean, A1> LeanArgs<'lean> for (A1,)

where A1: LeanAbi<'lean>,

const ARITY: usize = 1

impl<'lean, A1, A2> LeanArgs<'lean> for (A1, A2)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>,

const ARITY: usize = 2

impl<'lean, A1, A2, A3> LeanArgs<'lean> for (A1, A2, A3)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>,

const ARITY: usize = 3

impl<'lean, A1, A2, A3, A4> LeanArgs<'lean> for (A1, A2, A3, A4)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>,

const ARITY: usize = 4

impl<'lean, A1, A2, A3, A4, A5> LeanArgs<'lean> for (A1, A2, A3, A4, A5)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>,

const ARITY: usize = 5

impl<'lean, A1, A2, A3, A4, A5, A6> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>,

const ARITY: usize = 6

impl<'lean, A1, A2, A3, A4, A5, A6, A7> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>,

const ARITY: usize = 7

impl<'lean, A1, A2, A3, A4, A5, A6, A7, A8> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7, A8)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>,

const ARITY: usize = 8

impl<'lean, A1, A2, A3, A4, A5, A6, A7, A8, A9> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7, A8, A9)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>,

const ARITY: usize = 9

impl<'lean, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>,

const ARITY: usize = 10

impl<'lean, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>, A11: LeanAbi<'lean>,

const ARITY: usize = 11

impl<'lean, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12> LeanArgs<'lean> for (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12)

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>, A11: LeanAbi<'lean>, A12: LeanAbi<'lean>,

const ARITY: usize = 12

Implementors