Nuprl Definition : per-close

per-close{i:l}(Term;EQ;ts;T;T';eq) ==
  pRec(candidate-type-system{i:l, i:l}(Term)
  × Term
  × Term
  × term-equality{i:l}(Term);close.λp.let ts,T,T',eq = p

                                      in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (close <ts, T, T', eq>);T;T';e\000Cq)  ;<ts

                                                                                                               , T

                                                                                                               , T'

                                                                                                               , eq>)

Definitions occuring in Statement : per-eq-def: per-eq-def{i:l}(Term;EQ;ts;T;T';eq), candidate-type-system: candidate-type-system{i:l,j:l}(Term), term-equality: term-equality{i:l}(Term), parameterized-rec: pRec(C;x.B[x];c), spreadn: spread4, or: P ∨ Q, apply: f a, lambda: λx.A[x], pair: <a, b>, product: x:A × B[x]
Definitions occuring in definition : parameterized-rec: pRec(C;x.B[x];c), candidate-type-system: candidate-type-system{i:l,j:l}(Term), product: x:A × B[x], term-equality: term-equality{i:l}(Term), spreadn: spread4, or: P ∨ Q, per-eq-def: per-eq-def{i:l}(Term;EQ;ts;T;T';eq), lambda: λx.A[x], apply: f a, pair: <a, b>
FDL editor aliases : per-close

Latex:
per-close\{i:l\}(Term;EQ;ts;T;T';eq) == pRec(candidate-type-system\{i:l, i:l\}(Term) \mtimes{} Term \mtimes{} Term \mtimes{} term-equality\{i:l\}(Term);close.\mlambda{}p.let ts,T,T',eq = p in (ts T T' eq) \mvee{} per-eq-def\{i:l\}(Term;EQ;\mlambda{}T,T',eq. (close <ts , T , T' , eq>);T;T';eq) ;<ts , T , T' , eq>) Date html generated: 2016_05_15-PM-01_49_13 Last ObjectModification: 2015_09_23-AM-07_37_16 Theory : parameterized!rec Home Index