[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] A question



On Thu, Sep 25, 2003 at 05:10:20PM +0200, Grzegorz Bancerek wrote:

> /. has two arguments, 

This is what I thought but it actually has 4 arguments.

definition
  let X,D be set, p be PartFunc of X,D, i be set;
 assume  i in dom p;
 func p/.i -> Element of D equals
:: FINSEQ_4:def 4
    p.i;
end;


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr