Nuprl Rule : callbyvalueType
This rule proved as lemma rule_callbyvalue_type_true3 in file rules/rules_uni.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ 0 ≤ eval x = T in 0
BY callbyvalueType !parameter{i:l}
H ⊢ T ∈ Type
Definitions occuring in rule :
sqle: s ≤ t,
callbyvalue: callbyvalue,
natural_number: $n,
member: t ∈ T,
universe: Type,
axiom: Ax
Latex:
H \mvdash{} 0 \mleq{} eval x = T in 0
BY callbyvalueType !parameter\{i:l\}
H \mvdash{} T \mmember{} Type
Date html generated:
2019_06_20-PM-04_12_27
Last ObjectModification:
2016_07_08-PM-03_49_02
Theory : rules
Home
Index