Function generate 

pub fn generate(
    toplevel: &Toplevel,
    theory: &Theory,
    ty: &TyV,
) -> (DiscreteDblModel, Namespace)

Generate a discrete double model from a type.

Precondition: ty must be valid in the empty context.