litex-lang 0.9.85-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;

/// Prove set equality by extensionality (`by extension …`).
#[derive(Clone)]
pub struct ByExtensionStmt {
    pub left: Obj,
    pub right: Obj,
    pub proof: Vec<Stmt>,
    pub line_file: LineFile,
}

impl fmt::Display for ByExtensionStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self.proof.len() {
            0 => write!(
                f,
                "{} {} {} {} {}",
                BY, EXTENSION, self.left, EQUAL, self.right
            ),
            _ => write!(
                f,
                "{} {} {} {} {}{}\n{}",
                BY,
                EXTENSION,
                self.left,
                EQUAL,
                self.right,
                COLON,
                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.proof, 1)
            ),
        }
    }
}

impl ByExtensionStmt {
    pub fn new(left: Obj, right: Obj, proof: Vec<Stmt>, line_file: LineFile) -> Self {
        ByExtensionStmt {
            left,
            right,
            proof,
            line_file,
        }
    }
}