---

{ Pi_term  Type }

{ Proof }

---

Definitions occuring in Statement :  pi_term: Pi_term,  member: t  T,  universe: Type
Definitions :  universe: Type,  member: t  T,  equal: s = t,  unit: Unit,  subtype_rel: A r B,  product: x:A  B[x],  union: left + right,  tag-by: zT,  or: P  Q,  function: x:A  B[x],  implies: P  Q,  rev_implies: P  Q,  and: P  Q,  iff: P  Q,  all: x:A. B[x],  ldag: LabeledDAG(T),  labeled-graph: LabeledGraph(T),  record: record(x.T[x]),  isect2: T1  T2,  record+: record+,  eclass: EClass(A[eo; e]),  fset: FSet{T},  isect: x:A. B[x],  b-union: A  B,  list: type List,  set: {x:A| B[x]} ,  top: Top,  true: True,  name: Name,  pi_prefix: pi_prefix(),  type-monotone: Monotone(T.F[T]),  so_lambda: x.t[x],  rec: rec(x.A[x]),  pi_term: Pi_term
Lemmas :  type-monotone_wf,  pi_prefix_wf,  subtype_rel_sum,  subtype_rel_simple_product,  name_wf,  subtype_rel_wf,  unit_wf

---

Pi\_term  \mmember{}  Type


Date html generated: 2011_08_17-PM-06_41_37
Last ObjectModification: 2010_09_24-PM-03_23_47

Home Index