diff options
Diffstat (limited to 'src/NewBaseSystem.v')
| -rw-r--r-- | src/NewBaseSystem.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 0e3dd4b75..40f7e3821 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -709,7 +709,7 @@ Section Ops. Let m := Eval compute in s - Associational.eval c. (* modulus *) Let sz2 := Eval compute in ((sz * 2) - 1)%nat. - Definition addT : + Definition add_sig : { add : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, let eval {n} := Positional.eval (n := n) wt in @@ -731,7 +731,7 @@ Section Ops. reflexivity. Defined. - Definition mulT : + Definition mul_sig : {mul : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, let eval {n} := Positional.eval (n := n) wt in @@ -771,7 +771,7 @@ Section Ops. End Ops. (* -Eval cbv [projT1 addT lift2_sig proj1_sig] in (projT1 addT). -Eval cbv [projT1 mulT lift2_sig proj1_sig] in - (fun m d div_mod => projT1 (mulT m d div_mod)). -*) +Eval cbv [proj1_sig add_sig lift2_sig] in (proj1_sig add_sig). +Eval cbv [proj1_sig mul_sig lift2_sig] in + (fun m d div_mod => proj1_sig (mul_sig m d div_mod)). +*)
\ No newline at end of file |