2288 ('wits:' (term +))? ('rel:' term)? |
2288 ('wits:' (term +))? ('rel:' term)? |
2289 "} |
2289 "} |
2290 *} |
2290 *} |
2291 |
2291 |
2292 |
2292 |
2293 (* NOTYET |
|
2294 subsubsection {* \keyw{bnf\_decl} |
2293 subsubsection {* \keyw{bnf\_decl} |
2295 \label{sssec:bnf-decl} *} |
2294 \label{sssec:bnf-decl} *} |
2296 |
2295 |
2297 text {* |
2296 text {* |
2298 %%% TODO: use command_def once the command is available |
2297 %%% TODO: use command_def once the command is available |
2299 \begin{matharray}{rcl} |
2298 \begin{matharray}{rcl} |
2300 @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"} |
2299 @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"} |
2301 \end{matharray} |
2300 \end{matharray} |
2302 |
2301 |
2303 @{rail " |
2302 @{rail " |
2304 @@{command bnf} target? dt_name |
2303 @@{command bnf_decl} target? @{syntax dt_name} |
|
2304 ; |
|
2305 @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix? |
|
2306 ; |
|
2307 @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')' |
|
2308 ; |
|
2309 @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')' |
2305 "} |
2310 "} |
2306 *} |
2311 |
2307 *) |
2312 Declares a fresh type and fresh constants (map, set, relator, cardinal bound) |
|
2313 and asserts the bnf properties for these constants as axioms. Additionally, |
|
2314 type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the |
|
2315 set function)---this is the only difference of @{syntax dt_name} compared to |
|
2316 the syntax used by the @{command datatype_new}/@{command codatatype} commands. |
|
2317 |
|
2318 The axioms are sound, since one there exists a bnf of any given arity. |
|
2319 *} |
2308 |
2320 |
2309 |
2321 |
2310 subsubsection {* \keyw{print\_bnfs} |
2322 subsubsection {* \keyw{print\_bnfs} |
2311 \label{sssec:print-bnfs} *} |
2323 \label{sssec:print-bnfs} *} |
2312 |
2324 |