Nuprl Definition : test-Spec
test-Spec() ==
[<"prog", [<"aprog", [inr Atom ]>; <"iterate", [inl inl "foo"]>; <"test", [inl inl "prop"]>]>;
<"foo", [<"afoo", [inr Atom ]>; <"bar", [inl inl "foo"]>; <"xx", [inl inl "prop"; inl inl "prog"]>]>;
<"prop", [<"aprop", [inr Atom ]>; <"false", [inr Unit ]>; <"implies", [inl inl "prop"; inl inl "prop"]>; <"box", [inl\000C inl "prog"; inl inl "prop"]>; <"diamond", [inl inl "foo"; inl inl "prop"]>]>]
Definitions occuring in Statement :
cons: [a / b],
nil: [],
unit: Unit,
pair: <a, b>,
inr: inr x ,
inl: inl x,
token: "$token",
atom: Atom
Definitions occuring in definition :
pair: <a, b>,
cons: [a / b],
nil: [],
token: "$token",
inl: inl x,
unit: Unit,
inr: inr x ,
atom: Atom
FDL editor aliases :
test-Spec
Latex:
test-Spec() ==
[<"prog", [<"aprog", [inr Atom ]> <"iterate", [inl inl "foo"]> <"test", [inl inl "prop"]>]>
<"foo", [<"afoo", [inr Atom ]> <"bar", [inl inl "foo"]> <"xx", [inl inl "prop"; inl inl "prog"]\000C>]>
<"prop"
, [<"aprop", [inr Atom ]> <"false", [inr Unit ]> <"implies", [inl inl "prop"; inl inl "prop"]>\000C <"box", [inl inl "prog"; inl inl "prop"]> <"diamond", [inl inl "foo"; inl inl "prop"]>]
>]
Date html generated:
2019_10_15-AM-10_47_57
Last ObjectModification:
2019_03_25-PM-01_43_15
Theory : tree_1
Home
Index