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

Reply via email to