Function prop::path_semantics::check_q

source · 
pub fn check_q<T, X>(_: Q<X, T>)
Expand description

Checks that X is qual to T.

Examples found in repository?
examples/ps_bool.rs (line 185)
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193

pub fn proof3<
    T: DeclBool1<Type, Zero>,
    X: LProp<N = Zero>,
    Type: LProp<N = Two>
>(
    f1: Mem<X>,
    f2: Mem<Inc<X>>,
    not: T::Not,
)
    where X: POrd<Inc<X>>,
          Inc<X>: POrd<Inc<Inc<X>>>
{
    let not_expr = T::def_not(not.clone(), f1);
    let not_expr2 = T::def_not(not, f2);
    match T::decide() {
        Left(eq_x_false) => {
            let x1 = not_expr.0(eq_x_false);
            let x2 = not_expr2.1(x1);
            check_q::<T::False, _>(x2)
        }
        Right(eq_x_true) => {
            let x1 = not_expr.1(eq_x_true);
            let x2 = not_expr2.0(x1);
            check_q::<T::True, _>(x2)
        }
    }
}