Skip to main content

bitvec_postprocess_norm

core_models::abstractions::bitvec

Function bitvec_postprocess_norm 

Source 
pub fn bitvec_postprocess_norm()
Expand description

This function is useful only for verification in F*. Used with postprocess_rewrite, this tactic:

  1. Applies a series of rewrite rules (the lemmas marked with REWRITE_RULE)
  2. Normalizes, bottom-up, every sub-expressions typed BitVec<_> inside the body of a function. This tactic should be used on expressions that compute a static permutation of bits.