Struct LeanEncoder 

pub(crate) struct LeanEncoder<'genv, 'tcx> {
    def_id: MaybeExternId,
    genv: GlobalEnv<'genv, 'tcx>,
    fun_defs: Vec<FunDef>,
    constants: Vec<ConstDef>,
    constraint: Constraint,
}

Fields

def_id: MaybeExternId

genv: GlobalEnv<'genv, 'tcx>

fun_defs: Vec<FunDef>

constants: Vec<ConstDef>

constraint: Constraint

Implementations

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

pub fn new( def_id: MaybeExternId, genv: GlobalEnv<'genv, 'tcx>, fun_defs: Vec<FunDef>, constants: Vec<ConstDecl>, constraint: Constraint, ) -> Self

pub fn fun_defs(&self) -> &[FunDef]

pub fn constraint(&self) -> &Constraint

pub fn constants(&self) -> &[ConstDef]

pub(crate) fn theorem_name(&self) -> String

fn proof_name(&self) -> String

fn generate_lake_project_if_not_present( &self, lean_path: &Path, project_name: &str, ) -> Result<(), Error>

fn generate_def_file( &self, lean_path: &Path, project_name: &str, ) -> Result<(), Error>

fn generate_proof_file_if_not_present( &self, lean_path: &Path, project_name: &str, ) -> Result<(), Error>

fn check_proof_help(&self, lean_path: &Path, project_name: &str) -> Result<()>

pub fn check_proof( &self, lean_path: &Path, project_name: &str, ) -> QueryResult<()>

fn snake_case_to_pascal_case(snake: &str) -> String

fn extract_const_defs( const_decls: Vec<ConstDecl>, constraint: &Constraint, ) -> Vec<ConstDef>

fn extract_const_def( const_decl: &ConstDecl, constraint: &Constraint, acc: &mut Vec<Expr>, )

Trait Implementations

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

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.