diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 545614301..8fef7d410 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -90,9 +90,9 @@ Module Associational. Definition carryterm (w fw:Z) (t:Z * Z) := if (Z.eqb (fst t) w) - then dlet t2 := snd t in - dlet d2 := div t2 fw in - dlet m2 := modulo t2 fw in + then dlet_nd t2 := snd t in + dlet_nd d2 := div t2 fw in + dlet_nd m2 := modulo t2 fw in [(w * fw, d2);(w,m2)] else [t]. @@ -661,11 +661,13 @@ Module Compilers. | @List.repeat ?A => let rA := type.reify A in constr:(@ident.List_repeat rA) - | @LetIn.Let_In ?A ?B - => let B := lazymatch (eval cbv beta in B) with fun _ => ?B => B end in - let rA := type.reify A in + | @LetIn.Let_In ?A (fun _ => ?B) + => let rA := type.reify A in let rB := type.reify B in constr:(@ident.Let_In rA rB) + | @LetIn.Let_In ?A ?B + => let dummy := match goal with _ => fail 1 "Let_In contains a dependent type λ as its second argument:" B end in + constr:(I : I) | @combine ?A ?B => let rA := type.reify A in let rB := type.reify B in @@ -866,11 +868,13 @@ Module Compilers. => let rT := type.reify T in constr:(@ident.nat_rect rT) | Nat.pred => ident.pred - | @LetIn.Let_In ?A ?B - => let B := lazymatch (eval cbv beta in B) with fun _ => ?B => B end in - let rA := type.reify A in + | @LetIn.Let_In ?A (fun _ => ?B) + => let rA := type.reify A in let rB := type.reify B in constr:(@ident.Let_In rA rB) + | @LetIn.Let_In ?A ?B + => let dummy := match goal with _ => fail 1 "Let_In contains a dependent type λ as its second argument:" B end in + constr:(I : I) | @Datatypes.list_rect ?A (fun _ => ?B) => let rA := type.reify A in let rB := type.reify B in |