litex-lang 0.9.86-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
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

use crate::prelude::*;
use std::fmt;

#[derive(Debug)]
pub struct StmtUnknown {
    pub detail: Option<Vec<String>>,
}

impl fmt::Display for StmtUnknown {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", UNKNOWN_COLON)?;
        if let Some(detail_lines) = &self.detail {
            if !detail_lines.is_empty() {
                write!(f, " {}", detail_lines.join("\n"))?;
            }
        }
        Ok(())
    }
}

impl StmtUnknown {
    pub fn new() -> Self {
        StmtUnknown { detail: None }
    }

    pub fn new_with_detail(detail: String) -> Self {
        Self::new_with_detail_lines(vec![detail])
    }

    pub fn new_with_detail_lines(detail_lines: Vec<String>) -> Self {
        if detail_lines.is_empty() {
            return StmtUnknown { detail: None };
        }
        StmtUnknown {
            detail: Some(detail_lines),
        }
    }

    pub fn detail_for_display(&self) -> String {
        self.detail
            .as_ref()
            .map(|lines| lines.join("\n"))
            .unwrap_or_default()
    }
}