Nuprl Definition : filling_term
fill cA [phi ⟶ u] a0 == fill comp-op-to-comp-fun(cA) [phi ⟶ u] a0
Definitions occuring in Statement :
fill_term: fill cA [phi ⟶ u] a0,
comp-op-to-comp-fun: comp-op-to-comp-fun(cA)
Definitions occuring in definition :
fill_term: fill cA [phi ⟶ u] a0,
comp-op-to-comp-fun: comp-op-to-comp-fun(cA)
FDL editor aliases :
filling_term
Latex:
fill cA [phi \mvdash{}\mrightarrow{} u] a0 == fill comp-op-to-comp-fun(cA) [phi \mvdash{}\mrightarrow{} u] a0
Date html generated:
2016_07_08-PM-07_13_56
Last ObjectModification:
2016_06_21-AM-11_18_25
Theory : cubical!type!theory
Home
Index