Helper functions for recognizing builtin literal values. This module focus on recognizing the standard representation used in Lean for these literals. It also provides support for the following exceptional cases.
- Raw natural numbers (i.e., natural numbers which are not encoded using
OfNat.ofNat
). - Bit-vectors encoded using
OfNat.ofNat
andBitVec.ofNat
. - Negative integers encoded using raw natural numbers.
- Characters encoded
Char.ofNat n
wheren
can be a raw natural number or anOfNat.ofNat
. - Nested
Expr.mdata
.
Returns some n
if e
is a raw natural number, i.e., it is of the form .lit (.natVal n)
.
Equations
Instances For
Return some (n, type)
if e
is an OfNat.ofNat
-application encoding n
for a type with name typeDeclName
.
Equations
Instances For
Return some n
if e
is a raw natural number or an OfNat.ofNat
-application encoding n
.
Equations
Instances For
Return some i
if e
OfNat.ofNat
-application encoding an integer, or Neg.neg
-application of one.
Equations
Instances For
Return some s
if e
is of the form .lit (.strVal s)
.
Equations
Instances For
Return some ⟨n, v⟩
if e
is an OfNat.ofNat
application encoding a Fin n
with value v
Equations
Instances For
Return some ⟨n, v⟩
if e
is:
- an
OfNat.ofNat
application - a
BitVec.ofNat
application - a
BitVec.ofNatLT
application that encode aBitVec n
with valuev
.
Equations
Instances For
Return some n
if e
is an OfNat.ofNat
-application encoding the UInt8
with value n
.
Equations
Instances For
Return some n
if e
is an OfNat.ofNat
-application encoding the UInt16
with value n
.
Equations
Instances For
Return some n
if e
is an OfNat.ofNat
-application encoding the UInt32
with value n
.
Equations
Instances For
Return some n
if e
is an OfNat.ofNat
-application encoding the UInt64
with value n
.
Equations
Instances For
If e
is a literal value, ensure it is encoded using the standard representation.
Otherwise, just return e
.
Equations
Instances For
Returns true
if e
is a literal value.
Equations
Instances For
Check if an expression is a list literal (i.e. a nested chain of List.cons
, ending at a List.nil
),
where each element is "recognised" by a given function f : Expr → MetaM (Option α)
,
and return the array of recognised values.
Equations
Instances For
Check if an expression is an array literal
(i.e. List.toArray
applied to a nested chain of List.cons
, ending at a List.nil
),
where each element is "recognised" by a given function f : Expr → MetaM (Option α)
,
and return the array of recognised values.
Equations
Instances For
Check if an expression is an array literal
(i.e. List.toArray
applied to a nested chain of List.cons
, ending at a List.nil
),
returning the array of Expr
values.