Re:Learn Coq in Y Minutes
by cjfd on Tuesday November 26, 2019 @09:21AM
(#21638468)
Actually, there are binary numbers in the coq standard library. N is in the library NArith and Z is in the library ZArith. Both are binary.
Coq is not meant to be a language for computation. If you only use natural numbers to state properties like forall a b: nat, a + b = b + a there is nothing to unfold about them and no need to worry about inefficient computation.
Coq is not meant to be a language for computation. If you only use natural numbers to state properties like forall a b: nat, a + b = b + a there is nothing to unfold about them and no need to worry about inefficient computation.