const package:vinyl

Build a record whose elements are derived solely from a constraint satisfied by each.

Build a record whose elements are derived solely from a list of constraint constructors satisfied by each.

Sometimes we may know something for all fields of a record, but when you expect to be able to each of the fields, you are then out of luck. Surely given ∀x:u.φ(x) we should be able to recover x:u ⊢ φ(x)! Sadly, the constraint solver is not quite smart enough to realize this and we must make it patently obvious by reifying the constraint pointwise with proof.

Sometimes we may know something for all fields of a record, but when you expect to be able to each of the fields, you are then out of luck. Surely given ∀x:u.φ(x) we should be able to recover x:u ⊢ φ(x)! Sadly, the constraint solver is not quite smart enough to realize this and we must make it patently obvious by reifying the constraint pointwise with proof.

Build a record whose elements are derived solely from a constraint satisfied by each.

Build a record whose elements are derived solely from a list of constraint constructors satisfied by each.

Constraint that all types in a type-level list satisfy a constraint.