/[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 3583 by kopylov, Mon Jul 2 22:34:20 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 189  Line 189 
189  prec prec_fun < prec_apply  prec prec_fun < prec_apply
190  prec prec_fun < prec_lambda  prec prec_fun < prec_lambda
191    
192  dform fun_df1 : parens :: "prec"[prec_fun] :: "fun"{'A; 'B} =  dform fun_df1 : "fun"{'A; 'B} = math_fun{'A; 'B}
193     slot["le"]{'A} " " rightarrow " " slot["lt"]{'B}  dform fun_df2 : "fun"{'A; x. 'B} = math_fun{'x; 'A; 'B}
   
 dform fun_df2 : parens :: "prec"[prec_fun] :: "fun"{'A; x. 'B} =  
    slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'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}} `" | "  "fun"{'A; x. 'B} `" }"
# Line 302  Line 299 
299   * @thysubsection{Typehood and equality}   * @thysubsection{Typehood and equality}
300   *   *
301   * The well-formedness of the very-dependent function   * The well-formedness of the very-dependent function
302   * requires that the domain type $A$ be a type, the the domain   * requires that the domain type $A$ be a type, that the domain
303   * be well-founded with some relation $R$, and that $B[f, x]$ be   * be well-founded with some relation $R$, and that $B[f, x]$ be
304   * a type for any restricted function $@rfun{f; y; @set{A; x; R[z, y]}; B[f, y]}$.   * a type for any restricted function $@rfun{f; y; @set{A; x; R[z, y]}; B[f, y]}$.
305   * @end[doc]   * @end[doc]

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26