10 Commits

Author	SHA1	Message	Date
Edwin Brady	1616879c3e	Some FFI documentation ... Explaining how to write the most basic Idris bindings for readline, taking account of how to allocate Strings in the completion callback. Also adds the basic API as a sample, which can be used as a starting point for other packages containing C bindings.	2020-03-03 23:23:49 +00:00
Edwin Brady	1bb028ae47	Update proof tutorial for Idris 2	2020-02-26 12:33:01 +00:00
Edwin Brady	1e567ab2d4	Document multiplicities in crash course	2020-02-26 11:22:55 +00:00
Edwin Brady	16ae7994e7	More documentation refreshing	2020-02-25 22:18:02 +00:00
Edwin Brady	0be0c27d1a	Update interpreter section of crash course	2020-02-25 21:49:26 +00:00
Edwin Brady	a70c0a6ef6	More tutorial updates	2020-02-25 21:37:48 +00:00
Edwin Brady	2967e9011f	Add implementation ... using syntax ... It's in the tutorial, and allows named implementations to use specific parent named implementations.	2020-02-25 21:29:39 +00:00
Edwin Brady	827c51e343	More documentation updates ... Some way through the interfaces docs, but "using" for named parent interfaces is not implemented yet.	2020-02-25 21:01:15 +00:00
Edwin Brady	28b7c62521	Finish update of typesfuns	2020-02-25 19:44:49 +00:00
Edwin Brady	4d146d2416	Some progress on updating the tutorial	2020-02-25 18:34:32 +00:00