Nuprl Definition : any def

We use any x for the witness of x:Void |- C  (no matter what C is).
The term ⌜any x⌝ must have type ⌜x:Void ⟶ C⌝, but any term has this type!
Therefore, we could define ⌜any x⌝ to be ⌜⊥⌝, but, because we sometimes
want to compute all the subterms of a extract term, it is safer to define
⌜any x⌝ to be a canonincal term. So we choose ⌜Ax⌝, the "simplest" canonical
term.⋅
any x ==  Ax


Definitions occuring in Statement :  axiom: Ax
Definitions occuring in definition :  axiom: Ax
Rules referencing :  voidElimination,  freeFromAtomAbsurdity
Latex:
any  x  ==    Ax


Date html generated: 2016_07_08-PM-04_46_59
Last ObjectModification: 2015_09_22-PM-05_44_51

Theory : call!by!value_1


Home Index