Nuprl Definition : dl-Spec
dl-Spec() ==
[<"prog", [<"aprog", [inr ℕ ]>; <"comp", [inl inl "prog"; inl inl "prog"]>; <"choose", [inl inl "prog"; inl inl "prog"\000C]>; <"iterate", [inl inl "prog"]>; <"test", [inl inl "prop"]>]>;
<"prop", [<"aprop", [inr ℕ ]>; <"false", [inr Unit ]>; <"implies", [inl inl "prop"; inl inl "prop"]>; <"and", [inl in\000Cl "prop"; inl inl "prop"]>; <"or", [inl inl "prop"; inl inl "prop"]>; <"box", [inl inl "prog"; inl inl "prop"]>; <"diamo\000Cnd", [inl inl "prog"; inl inl "prop"]>]>]
Definitions occuring in Statement :
cons: [a / b],
nil: [],
nat: ℕ,
unit: Unit,
pair: <a, b>,
inr: inr x ,
inl: inl x,
token: "$token"
Definitions occuring in definition :
inl: inl x,
cons: [a / b],
token: "$token",
pair: <a, b>,
nil: [],
unit: Unit,
inr: inr x ,
nat: ℕ
FDL editor aliases :
dl-Spec
Latex:
dl-Spec() ==
[<"prog"
, [<"aprog", [inr \mBbbN{} ]> <"comp", [inl inl "prog"; inl inl "prog"]> <"choose", [inl inl "prog"; i\000Cnl inl "prog"]> <"iterate", [inl inl "prog"]> <"test", [inl inl "prop"]>]
>
<"prop"
, [<"aprop", [inr \mBbbN{} ]> <"false", [inr Unit ]> <"implies", [inl inl "prop"; inl inl "prop"]> <"\000Cand", [inl inl "prop"; inl inl "prop"]> <"or", [inl inl "prop"; inl inl "prop"]> <"box", [inl inl \000C"prog"; inl inl "prop"]> <"diamond", [inl inl "prog"; inl inl "prop"]>]
>]
Date html generated:
2019_10_15-AM-11_39_03
Last ObjectModification:
2019_03_26-AM-11_16_04
Theory : dynamic!logic
Home
Index