Giter Club home page Giter Club logo

idris-tutorial's Introduction

An OLD Tutorial for Idris.

This tutorial has become deprecated in favour of a Sphinx based, readthedocs integrated, solution hosted on the main idris repository. You can find this repository online:

http://www.github.com/idris-lang/Idris-dev

This repository is left here for archival purposes.

idris-tutorial's People

Contributors

artella-coding avatar david-christiansen avatar dckc avatar domsj avatar edwinb avatar enolan avatar gavlegoat avatar janbessai avatar jfdm avatar jmitchell avatar jthemphill avatar lmarburger avatar pseudonom avatar raichoo avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

idris-tutorial's Issues

Ordering and parameters blocks

The user shaleh on Reddit pointed out that section 5.3 on parameters blocks doesn't explicitly state that the new parameters come before the ones specified on each definition.

--check flag looks like -check

The end of section 2.2 doesn't display the flag prefixes properly.

From #idris:

ziman: it's probably latex that converts "--" to an en-dash
jfdm: indeed it is
jfdm: you can get round it using \verb!--check!

Missing quantification in code sample

See idris-lang/Idris-dev#1502 where the following was reported:


It seems there's an error on the code example in 3.8.3 / Dependent Pairs:

data Exists : (A : Type) -> (P : A -> Type) -> Type where
    Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P

has error:

When elaborating type of Main.Ex_intro:
No such variable A

I think it should be:

data Exists : (A : Type) -> (P : A -> Type) -> Type where
    Ex_intro : {A : Type} -> {P : A -> Type} -> (a : A) -> P a -> Exists A P

Add ! notation

! notation is currently not documented anywhere except by example

Laziness

The tutorial needs to explain the new 'Lazy' type and implict Force/Delay

Functor class defines map, not fmap.

Change

instance Functor Eval where
    fmap f (MkEval g) = MkEval (\e => fmap f (g e))

to

instance Functor Eval where
    map f (MkEval g) = MkEval (\e => map f (g e))

Reduce code duplication

Use listings package and link to the provided examples within the tutorial instead of duplicating them.

Totality checking

Add an explanation that totality checking is not perfect (nor even particularly good yet). Too many people seem surprised when it doesn't work as well as they'd like.

Tutorial Updates

Update tutorial to account for bitrot since latest released version of Idris.

Of note the section on unit testing.

Add ePub/.mobi/HTML versions

It would be immensely useful to have even at least one of those available out of the box without having to clone the repo (or a fork really) and figure out a way to build it. PDF's aren't particularly nice for on-screen reading!

Add choose function to the tutorial

Currently the tutorial talks briefly about the so data type and using it to ensure some runtime check has been performed but it doesn't mention any ways to construct so types.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.