Skip to main content

assume_inc_path_level

prop::path_semantics

Function assume_inc_path_level 

Source 
pub fn assume_inc_path_level<N: Nat, A: LProp, B: LProp, C: LProp, D: LProp>() -> PSemNaive<IncLevel<A, N>, IncLevel<B, N>, IncLevel<C, N>, IncLevel<D, N>>
where
    <IncLevel<A, N> as LProp>::N: Lt<<IncLevel<C, N> as LProp>::N>,
    <IncLevel<B, N> as LProp>::N: Lt<<IncLevel<D, N> as LProp>::N>,
    (A::N, N): Add,
    (B::N, N): Add,
    (C::N, N): Add,
    (D::N, N): Add,
Expand description

Generates naive core axiom at increased path semantical proposition level.