Lines Matching defs:conj
146 fun extract_cons conj =
147 let val (cons_args, body) = strip_forall conj
164 fun get_def_info conj =
165 let val {lhs, rhs} = dest_eq conj
602 {cons = constructor, cons_range = return_type, conj = conjunct}
614 returns the conj found as well as exists_data with that conj
619 (datum as {cons, conj, cons_range})::exists_data) =
621 (conj, addlist (seen_data, exists_data))
638 (datum as {cons, conj, cons_range})::exists_data) =
640 helper (seen_data, conj::conjs, exists_data)
673 let val (conj, exists_data2) =
676 conj::(mk_Qtm_body (def_data, exists_data2))