diff options
| author | Brian Campbell | 2018-07-26 14:11:42 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-27 17:42:55 +0100 |
| commit | b0c78262e4c8a8670c6a111cb3bcac00dc445251 (patch) | |
| tree | d3a1d8b70a14a0600eed627221cd61591d3a10a3 /src | |
| parent | 313c004c1829700697ea2fe1281cc1f7afe5904a (diff) | |
Coq: patterns on bit literals
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 2729e7cd..5a903a40 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4036,6 +4036,8 @@ struct type rlit = | RL_unit + (* TODO: zero and one are currently replaced by RL_inf to deal with BU; + needs more careful thought about semantics of BU *) | RL_zero | RL_one | RL_true @@ -4053,8 +4055,8 @@ let string_of_rlit = function let rlit_of_lit (L_aux (l,_)) = match l with | L_unit -> RL_unit - | L_zero -> RL_zero - | L_one -> RL_one + | L_zero -> (*RL_zero*) RL_inf + | L_one -> (*RL_one*) RL_inf | L_true -> RL_true | L_false -> RL_false | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> RL_inf @@ -4063,8 +4065,8 @@ let rlit_of_lit (L_aux (l,_)) = let inv_rlit_of_lit (L_aux (l,_)) = match l with | L_unit -> [] - | L_zero -> [RL_one] - | L_one -> [RL_zero] + | L_zero -> (*[RL_one]*) [RL_inf] + | L_one -> (*[RL_zero]*) [RL_inf] | L_true -> [RL_false] | L_false -> [RL_true] | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> [RL_inf] |