3.1. Literals
Definition3.1.1
used by 0✓L∃∀N
Associated Lean declarations
-
CoreCpp.Typing.expr[complete] -
CoreCpp.Eval.expr[complete] -
CoreCpp.Eval.int32[complete]
An integer literal has type int and a boolean literal has type bool. Evaluation leaves the store unchanged, and the integer literal goes through the range check.
\dfrac{}{\Gamma \vdash n : \mathsf{int}}\;\textsf{(T-Lit)}
\dfrac{}{\Gamma \vdash b : \mathsf{bool}}\;\textsf{(T-BoolLit)}
\dfrac{}{\rho, \sigma \vdash n \Rightarrow \mathsf{int32}\,n, \sigma}\;\textsf{(Lit)}
\dfrac{}{\rho, \sigma \vdash b \Rightarrow \mathsf{bool}\,b, \sigma}\;\textsf{(BoolLit)}
Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.
Lean code for Definition3.1.1●3 definitions
Associated Lean declarations
-
CoreCpp.Typing.expr[complete]
-
CoreCpp.Eval.expr[complete]
-
CoreCpp.Eval.int32[complete]
Associated Lean declarations
-
CoreCpp.Typing.expr[complete] -
CoreCpp.Eval.expr[complete] -
CoreCpp.Eval.int32[complete]
-
opaquedefined in CoreCpp/Typing.leancomplete
opaque CoreCpp.Typing.expr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
opaque CoreCpp.Typing.expr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
Γ ⊢ e : τ
-
opaquedefined in CoreCpp/Eval.leancomplete
opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
ρ, σ ⊢ e ⇒ v, σ'
-
defdefined in CoreCpp/Eval.leancomplete
def CoreCpp.Eval.int32 (n : Int) : CoreCpp.M CoreCpp.Val
def CoreCpp.Eval.int32 (n : Int) : CoreCpp.M CoreCpp.Val
Range check for `int`. ``` n ∈ [−2³¹, 2³¹ − 1] n ∉ [−2³¹, 2³¹ − 1] ────────────────── ────────────────────── int32 n = int n int32 n = error (overflow) ```