Function prop::path_semantics::assume_path_level[−][src]

pub fn assume_path_level<A: LProp, B: Prop, C: LProp, D: Prop>(
) -> PSemNaive<A, B, C, D> where
    A::N: Lt<C::N>,

Generates naive core axiom using assumption on path semantical proposition levels.

This is safe because path semantical propositions uses the semantics that the core axiom holds between layers of propositions.

Function prop::path_semantics::assume_path_level⎘[−][src]