Commit 470116af authored by Mart Lubbers's avatar Mart Lubbers

Add eadts to syntax builtins

parent 1bd3179e
......@@ -20,6 +20,7 @@ builtin_syntax =
, bs_define_graph
, bs_dotdot
, bs_exists
, bs_eadt
, bs_forall
, bs_foreign
, bs_funcdep
......@@ -154,6 +155,19 @@ bs_exists =
, syntax_examples = [EX ":: List = E.e: Cons e List | Nil\nStart = Cons 5 (Cons 'a' (Cons \"abc\" Nil))"]
}
bs_eadt =
{ syntax_title = "extensible algebraic data types"
, syntax_patterns = ["..", "|"]
, syntax_code = [":: T | ..", ":: T = .."]
, syntax_description = "Extensible algebraic data types are ADT's that can be extended in other modules. One module can declare the ADT as extendible by adding the .. constructior. Other modules can then extend it. It is not possible to derive functions for EADTs"
, syntax_doc_locations = []
, syntax_examples = map EX
[ ":: T = .. //Declare T as an EADT"
, ":: T = C1 | .. //Declare T to be an EADT with at least the constructor C1"
, ":: T | C //Extend the EADT T with constructor C"
]
}
bs_forall =
{ syntax_title = "universal quantifier"
, syntax_patterns = ["A", "A.*"]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment