Function generate

pub fn generate(
    toplevel: &Toplevel,
    theory: &Theory,
    ty: &TyV,
) -> (DiscreteDblModel, HashMap<QualifiedName, QualifiedLabel>)

Generate a discrete double model from a type.

Precondition: ty must be valid in the empty context.