Skip to content

Verify Tez_repr identities

Daniel Hilst requested to merge verify-tez-repr-eq into master
  • Rename positive predicates to non_negative since they are including 0 and I need strict positive predicate excluding 0
  • Added identities of addition, multiplication, subtraction and division in Z at Environment/Proofs/Pervasives.v
  • Added identities of Tez_repr addition, multiplication, subtraction and division in Z
Edited by Daniel Hilst

Merge request reports