Lines Matching defs:string
7 | Fail of string;
15 val getError : ('a, 'b) p -> string;
17 val initialState : 'a list -> ('a,string) p;
44 | Failed of string;
53 | Fail of string;
150 val scan : string -> cmd list;
152 val test : cmd list -> (parsed_theory option * string);
179 {assumes: {name:string option, term:string} list,
180 fixes: {names:string list, tp:string} list};
185 datatype mixfix_data = Infix of string * int
186 |InfixL of string * int
187 |InfixR of string * int
188 |Binder of {template:string,
191 |Template of {template:string,
197 datatype arity = Arity of (string list option) * string;
198 datatype instance_data = InstanceA of string list * arity
199 |InstanceR of {name:string,rel:string,
200 parent:string};
201 datatype theory_body_elem = Context of string * theory_body_elem list
202 |DataType of (string list * (string *
203 (string * string list) list)) list
204 |Consts of (string * string) list
205 |Axioms of (string * string) list
206 |Lemma of {name: string option,
207 attrs: string list option,
208 target: string option,
209 statement: string,
211 proof: string}
212 |Theorem of {name: string option,
213 attrs: string list option,
214 target: string option,
215 statement: string,
217 proof: string}
218 |Class of {name:string,
219 parents:string list,
221 |Locale of {name:string,
222 parents:string list,
224 |TypeSynonym of string list *
225 (string * string)
226 |Function of {name: string,
227 tp: string,
228 def_eqs: string list}
230 names: (string*(string option)) list,
231 def_eqs: string list}
233 {name_tp:(string*string option) option,
234 eq:string,target:string option,
235 attrs:string list option}
236 |Notation of {modes:string list option,
237 notations:(string*mixfix_data) list}
238 |NoNotation of {modes:string list option,
239 notations:(string*mixfix_data) list}
240 |Interpretation of {name:string,
242 eqs:(string*string list),
243 proof:string}
244 |Instantiation of {names:string list,
246 |Instance of instance_data option * string
247 |Abbreviation of string
248 |Declaration of string
249 |Axiomatization of {names:string list,
250 tp: string,mixfix_data:mixfix_data option}
252 |Hide of {what:string*hide_what,
253 names:string list}
254 |MiscCmd of string * string
255 |CodeCmd of string * string;
257 header: string option,
258 name: string,
259 imports: string list,
260 keywords: (string list*string) option,
463 exception Test of string;
609 type named_term = (string * term)
611 val unlines : string list -> string
612 val unqualify : string -> string
614 val theory_of_string : string -> theory list -> theory
615 val theory_by_name : string -> theory
616 val name_of_theory : theory -> string
620 val consts_of : theory -> (string * typ) list
621 val datatypes_of : theory -> ((string * typ list *
622 (string * typ list) list) list) list
625 val functions_of : theory -> (string * typ *
629 val classes_of : theory -> (class * string list *
630 (string * term) list *
631 (string * typ) list) list
633 val locales_of : theory -> (string *
634 ((string * typ) * mixfix) list *
636 string list) list
639 val pretty_as_str : Pretty.T -> string
642 val repr_name : string -> Pretty.T
643 val repr_function : theory -> (string * typ *
645 val repr_class : theory -> (class * string list *
646 (string * term) list *
647 (string * typ) list) -> Pretty.T
648 val repr_locale : theory -> (string *
649 ((string * typ) * mixfix) list *
651 string list) -> Pretty.T
652 val repr_datatype : theory -> (string * typ list * (string *
657 (string * typ) list)
659 type theory_data = (string * named_term list * named_term list *
660 (string * typ) list * ((string * typ list *
661 (string * typ list) list) list) list *
662 (string * typ * (term list * term) list) list *
663 (class * string list * (string * term) list *
664 (string * typ) list) list *
665 (string * ((string * typ) * mixfix) list *
667 string list) list)
672 exception ExportError of string
678 exception ExportError of string
680 type named_term = string * term
682 type theory_data = (string * named_term list * named_term list *
683 (string * typ) list * ((string * typ list *
684 (string * typ list) list) list) list *
685 (string * typ * (term list * term) list) list *
686 (class * string list * (string * term) list *
687 (string * typ) list) list *
688 (string * ((string * typ) * mixfix) list *
690 string list) list)
706 (* Keep track of the number of theories created from a string *)
709 (* create a theory from a string of its body *)
886 (* ------------------------------ Represent as string *)