File: bitvector_definitions.v

package info (click to toggle)
coq-stdpp 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,696 kB
  • sloc: makefile: 52; sh: 35; sed: 1
file content (13 lines) | stat: -rw-r--r-- 401 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
From stdpp Require Import strings.
From stdpp.bitvector Require Import definitions.

Check "notation_test".
Check (BV 10 3 = BV 10 5).
Fail Check (BV 2 3 = BV 10 5).
Check (BV 2 3 =@{bvn} BV 10 5).
Check (4%bv = BV 4 4).
Check ((-1)%bv = Z_to_bv 7 (-1)).
Goal (-1 =@{bv 5} 31)%bv. compute_done. Qed.

Check "bvn_to_bv_test".
Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.