Skip to content

Commit

Permalink
add brief explanation of 'eq' shortcut
Browse files Browse the repository at this point in the history
  • Loading branch information
jmid committed Feb 13, 2015
1 parent ca4ce75 commit 08705f1
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,15 @@ In addition LCheck provides a number of helper lattices:
- MkListLattice: a functor for building list lattices ordered entry-wise.


For more complex lattices containing syntactically different elements with the
same meaning (concretization or denotation), one can simply choose to implement
'eq' as a test for ordering in both directions:

let eq e e' = leq e e' && leq e' e

As a consequence the anti-symmetry from 'GenericTests' will be vacuously true.


The embedded DSLs:
------------------

Expand Down

0 comments on commit 08705f1

Please sign in to comment.