Binary integers in lean

Stream: new members

[cbailey]

WRT reasoning about programs, Is there any reason to use the binary integer representations in Mathlib ala ZArith in Lean outside of reasoning about bitwise operations? It says in the comments that their use is discouraged since Lean doesn't share Coq's reliance on kernel reduction; does Lean have some evaluation strategy for making functions written with Z and N run in non-linear time? Thanks for any help!

[Kenny Lau]

so if you try to use norm_num to prove that 10+11=21 for real numbers, they use bitwise addition

[Andrew Ashworth]

Lean's kernel has special optimized versions of nat and int when used with #eval

[Andrew Ashworth]

iirc

[Andrew Ashworth]

if you're trying to do meta-programming or reflection, then use zarith

[cbailey]

Thank you.