norm_num
extensions for Nat.log
and Nat.clog
#
This module defines norm_num
extensions for Nat.log
and Nat.clog
.
Given the natural number literals eb
and en
, returns Nat.log eb en
as a natural number literal and an equality proof.
Panics if ex
or en
aren't natural number literals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluates the Nat.log
function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given the natural number literals eb
and en
, returns Nat.clog eb en
as a natural number literal and an equality proof.
Panics if ex
or en
aren't natural number literals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluates the Nat.clog
function.
Equations
- One or more equations did not get rendered due to their size.