/[mojave]/metaprl/theories/itt/itt_rfun.ml
ViewVC logotype

Diff of /metaprl/theories/itt/itt_rfun.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3590 by nogin, Thu Apr 25 15:28:40 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 193  Line 193 
193  dform fun_df2 : "fun"{'A; x. 'B} = math_fun{'x; 'A; 'B}  dform fun_df2 : "fun"{'A; x. 'B} = math_fun{'x; 'A; 'B}
194    
195  dform fun_df3 : rfun{'A; f, x. 'B} =  dform fun_df3 : rfun{'A; f, x. 'B} =
196     "{" " " slot{bvar{'f}} `" | "  "fun"{'A; x. 'B} `" }"     "{" " " slot{bvar{'f}} mid  "fun"{'A; x. 'B} `" }"
197    
198  dform apply_df : parens :: "prec"[prec_apply] :: apply{'f; 'a} =  dform apply_df : parens :: "prec"[prec_apply] :: apply{'f; 'a} =
199     slot["lt"]{'f} " " slot["le"]{'a}     slot["lt"]{'f} " " slot["le"]{'a}

Legend:
Removed from v.3590  
changed lines
  Added in v.3591

  ViewVC Help
Powered by ViewVC 1.1.26