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
use crate::prelude::*;

impl Runtime {
    pub fn verify_obj_well_defined_with_its_local_def(
        &mut self,
        params_def: Vec<ParamGroupWithSet>,
        define_params_to_be_param_obj_type: ParamObjType,
        obj: Obj,
    ) -> Result<(), RuntimeError> {
        self.run_in_local_env(|rt| {
            for param_def in params_def.iter() {
                rt.define_params_with_set_in_scope(param_def, define_params_to_be_param_obj_type)?;
            }
            rt.verify_obj_well_defined_and_store_cache(&obj, &VerifyState::new(0, false))
        })
    }
}