Zulip Chat Archive

Stream: new members

Topic: Binary integers in lean


view this post on Zulip cbailey (Nov 15 2018 at 16:20):

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!

view this post on Zulip Kenny Lau (Nov 15 2018 at 19:02):

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

view this post on Zulip Andrew Ashworth (Nov 15 2018 at 19:58):

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

view this post on Zulip Andrew Ashworth (Nov 15 2018 at 19:58):

iirc

view this post on Zulip Andrew Ashworth (Nov 15 2018 at 19:59):

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

view this post on Zulip cbailey (Nov 15 2018 at 22:56):

Thank you.


Last updated: May 16 2021 at 20:13 UTC