Nuprl Definition : comp_trm
comp_trm(Gamma;cA;phi;u;a0) == comp cA [phi ⊢→ u] a0
Definitions occuring in Statement :
comp_term: comp cA [phi ⊢→ u] a0
Definitions occuring in definition :
comp_term: comp cA [phi ⊢→ u] a0
FDL editor aliases :
comp_trm
Latex:
comp\_trm(Gamma;cA;phi;u;a0) == comp cA [phi \mvdash{}\mrightarrow{} u] a0
Date html generated:
2016_05_19-AM-10_42_27
Last ObjectModification:
2016_04_26-AM-10_52_01
Theory : cubical!type!theory
Home
Index