Equations
Instances For
Given e
of the form lhs ≤ rhs
where lhs
and rhs
have type Nat
,
returns (lhs, rhs)
where lhs
and rhs
are Int.OfNat.Expr
.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Given e
of type Int
, tries to compute a : Int.OfNat.Expr
s.t.
a.denoteAsInt ctx
is e
If e
is of the form a.denoteAsInt ctx
for some a
and ctx
,
assert that e
is nonnegative.
Equations
Instances For
Given x
whose denotation is e
, if e
is of the form NatCast.natCast a
,
asserts that it is nonnegative.