[Civl] Ticket example

[shazqadeer]

• add test driver back
• remove nil in favor of Option
• use Lval and Lset

[bkragl]

Just one comment/question about the changed choice function.

[bkragl]

Why ditch the Set_ prefix and working with the Set wrapper type?

Would it be of any use to make the return type Option<T> and return None for empty sets instead of an unconstrained T?

[shazqadeer]

The earlier Set_Choose was defined on the type Set T of finite sets. In the ticket sample, I want to make a choice on the domain of an Lset which is [T]bool. So I thought I would generalize Set_Choose to Choice allowing the idea to work on any set, finite or infinite.

Would it be of any use to make the return type Option and return None for empty sets instead of an unconstrained T?

Currently, I don't see any advantage.

[bkragl]

Oh, I did not realize that Set is for finite sets. Otherwise the domain of an Lset could have been a Set.

[bkragl]

Oh, I did not realize that Set is for finite sets. Otherwise the domain of an Lset could have been a Set.

[shazqadeer]

Set T is defined here. It was added just so we could consolidate reasoning about cardinality of finite sets in one place.