​It's like asking where are the oxygen molecules in the air you breathe.

   f=: +/@i. = 2&!
   f"0 i.20
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1

See also *A Letter from Dijkstra on APL
<http://archive.vector.org.uk/art10501260> .*






On Sat, Mar 1, 2014 at 7:55 PM, km <[email protected]> wrote:

> One "identity" in J is that ([: f g) -: f@:g (always returns 1).  What
> are some others?
>
> --Kip Murray
>
> Sent from my iPad
>
> > On Mar 1, 2014, at 8:41 PM, Raul Miller <[email protected]> wrote:
> >
> > Two languages which go even more heavily into "proof" territory are (if I
> > recall correctly) Agda, and Coq.
> >
> > They also have some interesting aspects that I would like to see in a "J
> > subset compiler".
> >
> > Thanks,
> >
> > --
> > Raul
> >
> >
> > On Sat, Mar 1, 2014 at 8:30 PM, David Lambert <[email protected]
> >wrote:
> >
> >> Mentioning "proof" in j conversation rolls easily off the pen.  Not so
> >> with other computer languages I've used.
> >>
> >>   (,&#~.) HASHES  NB. prove the hashes are unique.  (tallies agree)
> >> 6 6
> >>
> >> http://forums.devshed.com/showpost.php?p=2927271&postcount=4
> >> ----------------------------------------------------------------------
> >> For information about J forums see http://www.jsoftware.com/forums.htm
> > ----------------------------------------------------------------------
> > For information about J forums see http://www.jsoftware.com/forums.htm
> ----------------------------------------------------------------------
> For information about J forums see http://www.jsoftware.com/forums.htm
>
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm

Reply via email to