module FStar.Tactics.CanonCommMonoidSimple

fsdoc: no-summary-found

fsdoc: no-comment-found

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