diff options
| -rw-r--r-- | test-suite/success/cbv_let.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v new file mode 100644 index 0000000000..861a73a64e --- /dev/null +++ b/test-suite/success/cbv_let.v @@ -0,0 +1,34 @@ +Record T : Type := Build_T { f : unit; g := pair f f; }. + +Definition t : T := {| f := tt; |}. + +Goal match t return unit with Build_T f g => f end = tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal match t return prod unit unit with Build_T f g => g end = pair tt tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal forall (x : T), + match x return prod unit unit with Build_T f g => g end = + pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end. +Proof. +cbv. +destruct x. +reflexivity. +Qed. + +Record U : Type := Build_U { h := tt }. + +Definition u : U := Build_U. + +Goal match u with Build_U h => h end = tt. +Proof. +cbv. +reflexivity. +Qed. |