diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-02 10:58:28 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0ab98d3380033b58162015656f435ae90b936856 (patch) | |
| tree | 38a17503ccbc5fd51d473f458e782812360ed5b1 /src/Reflection/MultiSizeTest2.v | |
| parent | 7f0ba34481f59db0cf430d7a08b8b65d953eb803 (diff) | |
make 8.5 happy
Diffstat (limited to 'src/Reflection/MultiSizeTest2.v')
| -rw-r--r-- | src/Reflection/MultiSizeTest2.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v index 575b8978a..4bac3d14c 100644 --- a/src/Reflection/MultiSizeTest2.v +++ b/src/Reflection/MultiSizeTest2.v @@ -158,6 +158,7 @@ Example ex1 : Expr base_type op (Arrow Unit TNat) := fun var => LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => Op (Plus Nat) (Pair (Var c) (Var c)))))). +(* Example ex1f : Expr base_type op (Arrow (TNat * TNat) TNat) := fun var => Abs (fun a0b0 : interp_flat_type _ (TNat * TNat) => let a0 := fst a0b0 in let b0 := snd a0b0 in @@ -179,3 +180,4 @@ Eval compute in ex1fb. Definition ex1fb' := Boundify ex1f (64, 64)%core. Eval compute in ex1fb'. +*)
\ No newline at end of file |