Struct LeanEncoder 

pub struct LeanEncoder<'genv, 'tcx> {
    genv: GlobalEnv<'genv, 'tcx>,
    path: PathBuf,
    project: String,
    defs_file_name: String,
    pretty_var_map: PrettyMap<LocalVar>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

path: PathBuf

project: String

defs_file_name: String

pretty_var_map: PrettyMap<LocalVar>

Implementations

impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx>

pub fn new( genv: GlobalEnv<'genv, 'tcx>, pretty_var_map: PrettyMap<LocalVar>, ) -> Self

fn generate_lake_project_if_not_present(&self) -> Result<(), Error>

fn generate_sort_def_file_if_not_present( &self, sort: &SortDecl, ) -> Result<(), Error>

fn generate_func_def_file_if_not_present( &self, fun: &ConstDecl, has_opaque_sorts: bool, has_data_decls: bool, ) -> Result<(), Error>

fn generate_opaque_sort_files(&self, sorts: &[SortDecl]) -> Result<(), Error>

fn generate_struct_defs_file( &self, data_decls: &[DataDecl], has_opaque_sorts: bool, ) -> Result<(), Error>

fn generate_opaque_func_files( &self, funs: &[ConstDecl], has_opaque_sorts: bool, has_data_decls: bool, ) -> Result<(), Error>

fn generate_func_defs_file( &self, func_defs: &[FunDef], has_opaque_sorts: bool, has_data_decls: bool, has_opaque_funcs: bool, ) -> Result<(), Error>

fn generate_lib_file(&self) -> Result<(), Error>

pub fn encode_defs( &self, opaque_sorts: &[SortDecl], opaque_funs: &[ConstDecl], data_decls: &[DataDecl], func_defs: &[FunDef], ) -> Result<(), Error>

fn theorem_path(&self, theorem_name: &str) -> PathBuf

fn generate_theorem_file( &self, theorem_name: &str, kvars: &[KVarDecl], cstr: &Constraint, ) -> Result<(), Error>

fn generate_proof_file_if_not_present( &self, def_id: MaybeExternId, theorem_name: &str, ) -> Result<(), Error>

pub fn encode_constraint( &self, def_id: MaybeExternId, kvars: &[KVarDecl], cstr: &Constraint, ) -> Result<(), Error>

fn check_proof_help(&self, theorem_name: &str) -> Result<()>

pub fn check_proof(&self, def_id: MaybeExternId) -> QueryResult<()>

fn snake_case_to_pascal_case(snake: &str) -> String