Nuprl Definition : pres-v
pres-v(G;phi;t;t0;cT) == fill cT [phi ⊢→ t] t0
Definitions occuring in Statement :
fill_term: fill cA [phi ⊢→ u] a0
Definitions occuring in definition :
fill_term: fill cA [phi ⊢→ u] a0
FDL editor aliases :
pres-v
Latex:
pres-v(G;phi;t;t0;cT) == fill cT [phi \mvdash{}\mrightarrow{} t] t0
Date html generated:
2016_05_19-AM-10_58_17
Last ObjectModification:
2016_04_15-PM-10_04_49
Theory : cubical!type!theory
Home
Index