Skip to content
Snippets Groups Projects
Commit eb662f83 authored by Michael Sammler's avatar Michael Sammler
Browse files

Fix bitvector tests for coq#16748

parent f8d00956
No related branches found
No related tags found
1 merge request!421Fix bitvector tests for coq#16748
Pipeline #74135 passed
...@@ -5,7 +5,7 @@ Check "notation_test". ...@@ -5,7 +5,7 @@ Check "notation_test".
Check (BV 10 3 = BV 10 5). Check (BV 10 3 = BV 10 5).
Fail Check (BV 2 3 = BV 10 5). Fail Check (BV 2 3 = BV 10 5).
Check (BV 2 3 =@{bvn} BV 10 5). Check (BV 2 3 =@{bvn} BV 10 5).
Fail Goal (BV 2 4 = BV 2 5). Fail Goal (BV 2 4 = BV 2 3).
Check "bvn_to_bv_test". Check "bvn_to_bv_test".
Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort. Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment