blob: 115c1f95bd2c3f5b7985aaca873f07456d31b7ac (
plain)
1
2
3
4
|
Require Coq.ZArith.BinInt.
Declare Reduction comp := vm_compute.
Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl).
Definition foo1 := Eval comp in (foo0, foo0).
|