From 1fb1958d505974a3864322d3f10f5dfa042f363a Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 27 Feb 2017 10:51:56 -0500 Subject: changed names of ops in NewBaseSystem to reflect that they are sig and not sigT --- src/NewBaseSystem.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/NewBaseSystem.v') 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 -- cgit v1.2.3