litex-lang 0.9.65-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
use crate::prelude::*;

pub(super) fn impossible_proof_error_message(
    impossible_fact: &AtomicFact,
    option_case_fact_string: Option<String>,
) -> String {
    match option_case_fact_string {
        Some(case_fact) => format!(
            "failed to prove impossible `{}` under case `{}`",
            impossible_fact, case_fact
        ),
        None => format!("failed to prove impossible `{}`", impossible_fact),
    }
}