Function chalk_solve::clauses::program_clauses::well_formed_program_clauses

source · 
fn well_formed_program_clauses<'a, I, Wc>(
    builder: &'a mut ClauseBuilder<'_, I>,
    ty: Ty<I>,
    where_clauses: Wc,
)
where
    I: Interner,
    Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>,
Expand description

Generates the “well-formed” program clauses for an applicative type with the name type_name. For example, given a struct definition:

ⓘ
struct Foo<T: Eq> { }

we would generate the clause:

forall<T> {
    WF(Foo<T>) :- WF(T: Eq).
}

§Parameters

  • builder – the clause builder. We assume all the generic types from Foo are in scope
  • type_name – in our example above, the name Foo
  • where_clauses – the list of where clauses declared on the type (T: Eq, in our example)