No other cites to report in EditorDoc | |
scan_lib_file | Def ScanLibFile: FileName Def AtFirst atfirst Eof ifeof WithNextifnoteof Def help Def == let fname complete_file_name FileName in Def == {Open the file then apply the function to Eof predicate and a Next Def == {operator, which returns the first entry, then advances the file. } Def == new_load_file fname Def == (Eof.Next. Def == (letrec ScanRest SoFar Def == (letrec if Eof () then ifeof else Def == (letrec let fobtok,fobkind,fobterm,fobruletree,fobload Next () , Def == (letrec let fobload tk Def == (letrec let fobload tk ; Def == (letrec let (if fobkind=`THM` thendo complete_thm_load tk) , Def == (letrec let fobstr tok_to_string fobtok , Def == (letrec let tagterm () Def == (letrec let plug_enum Def == (letrec let #COVER Def == (letrec let # 1 2 from 4 3 : term Def == (letrec let # Def == (letrec let IMP:IMPLODE Def == (letrec let IMP:Icomment{pre:s}( Def == (letrec let IMP:IcommentIMPLODE variable{3:v}; IMPLODE Def == (letrec let IMP:IcommentIMPLODE variable{3:v}; Ivariable{1:v} Def == (letrec let IMP:IcommentIMPLODE variable{2:v} from IMPLODE Def == (letrec let IMP:IcommentIMPLODE variable{2:v} from Ivariable{4:v}) Def == (letrec let [tok_to_word fobkind Def == (letrec let ;make_obref fobtok Def == (letrec let ;fobterm Def == (letrec let ;string_to_word fname] in Def == (letrec ifnoteof in Def == (ScanRest atfirst) |
ml_implode_term | Def IMP:T == edit_implode_all T |
ml_apply | Def a b == ((a)(b)) |
ml_nil | Def [] == [] |
ml_cons | Def a.b == ((a).(b)) |
ml_doif | Def if a thendo b == if a then do b else () |
ml_theunit | Def () == () |
ml_letin | Def let$mod a b in c == let$mod a b in c |
ml_tok | Def `$tok` == `$tok` |
ml_eq | Def a=b == ((a)=(b)) |
ml_seq | Def a ; b == ((a);(b)) |
ml_pair | Def a,b == ((a),(b)) |
ml_if | Def if a then b else c == if a then b else c |
ml_lambda | Def a.b == (\a.(b)) |
ml_decl | Def a b == a=(b) |
ml_letin_wrap | Def let$mod D in c == let$mod D in (c) |
ml_do_unop | Def do X == (do (X)) |
ml_test | Def if a $then b $else c == if (a) $then (b) $else c |
ml_parens | Def (a) == (a) |
ml_toko | Def `s` == `s` |
Syntax: | AtFirst atfirst Eof ifeof WithNextifnoteof help | has structure: |
About: