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
15
16
17
18
19

use crate::prelude::*;

impl Runtime {
    pub fn exec_def_abstract_prop_stmt(
        &mut self,
        def_abstract_prop_stmt: &DefAbstractPropStmt,
    ) -> Result<StmtResult, RuntimeError> {
        self.store_def_abstract_prop(def_abstract_prop_stmt)
            .map_err(|e| {
                short_exec_error(def_abstract_prop_stmt.clone().into(), "", Some(e), vec![])
            })?;
        Ok((NonFactualStmtSuccess::new(
            def_abstract_prop_stmt.clone().into(),
            InferResult::new(),
            vec![],
        ))
        .into())
    }
}