litex-lang 0.9.6-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

use crate::prelude::*;
use std::result::Result;

impl Runtime {
    pub fn exec_fact(&mut self, fact: &Fact) -> Result<StmtResult, RuntimeError> {
        let result = self.verify_fact_return_err_if_not_true(fact, &VerifyState::new(0, false))?;

        let infer_result = self.store_fact_without_well_defined_verified_and_infer(fact.clone())?;

        Ok(result.with_infers(infer_result))
    }
}