Enum LeanFile 

pub enum LeanFile {
    Basic,
    Fluxlib,
    OpaqueSort(String),
    Struct(String),
    OpaqueFun(String),
    Fun(String),
    Vc(DefId),
    Proof(DefId),
}

Different kinds of Lean files

Variants

Basic

“Root” of the lean project, importing all the generated proofs

Fluxlib

“builtin” definitions

OpaqueSort(String)

(human) opaque flux sorts, to be defined by the user in Lean

Struct(String)

(machine) sorts generated from flux definitions

OpaqueFun(String)

(human) opaque flux functions, to be defined by the user in Lean

Fun(String)

(machine) functions generated from flux definitions

Vc(DefId)

(machine) propositions holding the flux VCs

Proof(DefId)

(human) interactively written proofs of flux VCs

Implementations

impl LeanFile

fn kind(&self) -> FileKind

fn segments(&self, genv: GlobalEnv<'_, '_>) -> Vec<String>

fn path(&self, genv: GlobalEnv<'_, '_>) -> PathBuf

All paths should be generated here

Trait Implementations

impl Clone for LeanFile

fn clone(&self) -> LeanFile

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LeanFile

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

Formats the value using the given formatter.

impl Hash for LeanFile

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for LeanFile

fn eq(&self, other: &LeanFile) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for LeanFile

impl StructuralPartialEq for LeanFile