module FStar.Tactics.CanonCommMonoid

fsdoc: no-summary-found

fsdoc: no-comment-found

*** Expression syntax 
*** Expression denotation 
*** Flattening expressions to lists of variables 
*** Permuting the lists of variables
       by swapping adjacent elements 
*** Sorting variables is a correct permutation
       (since it can be done by swaps) 
*** Canonicalization tactics 
*** Examples