Struct LeanEncoder 

pub struct LeanEncoder<'genv, 'tcx, 'a> {
    genv: GlobalEnv<'genv, 'tcx>,
    lean_path: &'a Path,
    project_name: String,
    defs_file_name: String,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

lean_path: &'a Path

project_name: String

defs_file_name: String

Implementations

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

pub fn new( genv: GlobalEnv<'genv, 'tcx>, lean_path: &'a Path, project_name: String, defs_file_name: String, ) -> Self

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

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

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

fn generate_typeclass_file( &self, sorts: &[SortDecl], funs: &[ConstDecl], data_decls: &[DataDecl], ) -> Result<(), Error>

fn generate_defs_file( &self, func_defs: &[FunDef], has_opaques: 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 generate_theorem_file( &self, theorem_name: &str, kvars: &[KVarDecl], cstr: &Constraint, ) -> Result<(), Error>

fn generate_proof_file_if_not_present( &self, 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