Language.Lean.Env

Operations for working with Lean environments.

Documentation

data Env

A Lean environment

Instances

IsLeanValue Env (Ptr Env)

data TrustLevel

The level of trust associated with an environment.

Instances

Eq TrustLevel

Num TrustLevel

Ord TrustLevel

Show TrustLevel

trustHigh :: TrustLevel

Trust level for all macros implemented in Lean.

Constructing and manipulating environments.

standardEnv :: TrustLevel -> Env

Create an empty standard environment with the given trust level.

hottEnv :: TrustLevel -> Env

Create an empty hott environment with the given trust level.

envAddUniv :: Name -> Env -> Env

Add a new global universe with the given name.

envAddDecl :: CertDecl -> Env -> Env

Adding the given certified declaration to the environment.

envReplaceAxiom :: CertDecl -> Env -> Env

Replace the axiom that has the name of the given certified declaration with the certified declaration.

This procedure throws an exception if

• The theorem was certified in an environment which is not an ancestor of the environment.
• The environment does not contain an axiom with the given name.

Projections

envTrustLevel :: Env -> TrustLevel

The trust level of the given environment.

envContainsProofIrrelProp :: Env -> Bool

Return true if the given environment has a proof irrelevant Prop such as Type.{0}.

envIsImpredicative :: Env -> Bool

Return true iff in the given environment Prop is impredicative.

envContainsDecl :: Env -> Name -> Bool

Return true iff the environment contains a declaration with the name.

envLookupDecl :: Name -> Env -> Maybe Decl

Lookup the declaration with the given name in the environment.

envContainsUniv :: Env -> Name -> Bool

Return true iff the environment contains a global universe with the name.

envIsDescendant :: Env -> Env -> Bool

x `envIsDescendant' y return true x is a descendant of y, that is, x was created by adding declarations to y.

Operations

envForget :: Env -> Env

Return a new environment, where its "history" has been truncated/forgotten. That is, envForget x envIsDescendant y will return false for any environment y that is not pointer equal to the result envForget x.

envDecls :: Fold Env Decl

A fold over the declaration in the environment.

forEnvDecl_ :: Env -> (Decl -> IO ()) -> IO ()

Run an IO action on each declaration in the environment.

envUnivs :: Fold Env Name

Fold over the global universes in the environment.

forEnvUniv_ :: Env -> (Name -> IO ()) -> IO ()

Run an IO action on each universe in the environment.