Right [ TokenDoctype ( Doctype "html" Nothing ( InternalSubset { _elementTypes = [] , _attributeLists = [] , _generalEntities = [] , _parameterEntities = [] , _notations = [] , _instructions = [] } ) ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "html" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "lang" } ) [ ContentText "en" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "head" } ) [] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "title" } ) [] ) , TokenData [ ContentText "Idris: A Language for Type-Driven Development" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "title" } ) , TokenData [ ContentText " " ] , TokenEmptyElementTag ( EmptyElementTag ( QName { namePrefix = "" , nameLocal = "meta" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "charset" } ) [ ContentText "utf-8" ] ] ) , TokenData [ ContentText " " ] , TokenEmptyElementTag ( EmptyElementTag ( QName { namePrefix = "" , nameLocal = "link" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "rel" } ) [ ContentText "stylesheet" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/theme/css/main.css" ] , Attribute ( QName { namePrefix = "" , nameLocal = "type" } ) [ ContentText "text/css" ] ] ) , TokenData [ ContentText " " ] , TokenEmptyElementTag ( EmptyElementTag ( QName { namePrefix = "" , nameLocal = "link" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/" ] , Attribute ( QName { namePrefix = "" , nameLocal = "type" } ) [ ContentText "application/atom+xml" ] , Attribute ( QName { namePrefix = "" , nameLocal = "rel" } ) [ ContentText "alternate" ] , Attribute ( QName { namePrefix = "" , nameLocal = "title" } ) [ ContentText "Idris ATOM Feed" ] ] ) , TokenData [ ContentText " " ] , TokenComment "[if IE]> " , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h1" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "nav" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "ul" } ) [] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/index.html" ] ] ) , TokenData [ ContentText "Home" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/download.html" ] ] ) , TokenData [ ContentText "Download" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/example.html" ] ] ) , TokenData [ ContentText "Example" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/documentation.html" ] ] ) , TokenData [ ContentText "Documentation" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenComment "
  • Archives
  • " , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/category/news.html" ] ] ) , TokenData [ ContentText "News" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "ul" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "nav" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "header" } ) , TokenComment " /#banner " , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "section" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "content" ] , Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "body" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h1" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "entry-title" ] ] ) , TokenData [ ContentText "Idris: A Language for Type-Driven Development" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h1" } ) , TokenData [ ContentText " " ] , TokenComment " .. image:: images/profile.jpeg " , TokenData [ ContentText " " ] , TokenComment " :alt: [Shape Sorter Box] " , TokenData [ ContentText " " ] , TokenComment " :align: right " , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "Idris is a programming language designed to encourage " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "em" } ) [] ) , TokenData [ ContentText "Type-Driven Development" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "em" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "In type-driven development, types are tools for constructing programs. We treat the type as the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "em" } ) [] ) , TokenData [ ContentText "plan" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "em" } ) , TokenData [ ContentText " for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a small but powerful idea, enabling:" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "ul" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "simple" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenData [ ContentText "relationships to be expressed between values; for example, that two lists have the same length." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenData [ ContentText "assumptions to be made explicit and checked by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenData [ ContentText "if desired, properties of program behaviour to be formally stated and proven." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "ul" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "div" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "section" ] , Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "getting-started" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h2" } ) [] ) , TokenData [ ContentText "Getting Started" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h2" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "You can see some " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/example.html" ] ] ) , TokenData [ ContentText "small examples" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText ", then take a look at the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/documentation.html" ] ] ) , TokenData [ ContentText "documentation" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "div" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "div" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "section" ] , Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "community" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h2" } ) [] ) , TokenData [ ContentText "Community" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h2" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dl" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "docutils" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dt" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "strong" } ) [] ) , TokenData [ ContentText "Mailing list" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "strong" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dt" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dd" } ) [] ) , TokenData [ ContentText "Long-form discussion happens on the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://groups.google.com/forum/#!forum/idris-lang" ] ] ) , TokenData [ ContentText "mailing list" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dd" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dt" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "strong" } ) [] ) , TokenData [ ContentText "IRC" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "strong" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dt" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dd" } ) [] ) , TokenData [ ContentText "There is also an irc channel " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "tt" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "docutils literal" ] ] ) , TokenData [ ContentText "#idris" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "tt" } ) , TokenData [ ContentText " on " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "irc://chat.freenode.net/idris" ] ] ) , TokenData [ ContentText "freenode" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText ". Point your irc client to " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "tt" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "docutils literal" ] ] ) , TokenData [ ContentText "chat.freenode.net" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "tt" } ) , TokenData [ ContentText " then " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "tt" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "docutils literal" ] ] ) , TokenData [ ContentText "/join #idris" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "tt" } ) , TokenData [ ContentText ". Alternatively, there is a " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://webchat.freenode.net/" ] ] ) , TokenData [ ContentText "web interface" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dd" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dt" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "strong" } ) [] ) , TokenData [ ContentText "GitHub" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "strong" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dt" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dd" } ) [] ) , TokenData [ ContentText "The Idris source is available from our repository. Tools and code by the wider Idris community are available in a " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://github.com/idris-hackers" ] ] ) , TokenData [ ContentText "GitHub organisation" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dd" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dt" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "strong" } ) [] ) , TokenData [ ContentText "Slack" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "strong" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dt" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "dd" } ) [] ) , TokenData [ ContentText "There is an active " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "tt" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "docutils literal" ] ] ) , TokenData [ ContentText "#idris" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "tt" } ) , TokenData [ ContentText " channel on the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://functionalprogramming.slack.com/" ] ] ) , TokenData [ ContentText "Functional Programming" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText " Slack." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dd" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "dl" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "All participants in these forums are requested to abide by the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/pages/community-standards.html" ] ] ) , TokenData [ ContentText "community standards" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "Idris development is led by " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://www.type-driven.org.uk/edwinb/" ] ] ) , TokenData [ ContentText "Edwin Brady" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText " at the " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://www.cs.st-andrews.ac.uk" ] ] ) , TokenData [ ContentText "School of Computer Science, University of St Andrews" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "Many thanks to Heath Johns for designing the logo." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "div" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "div" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "section" ] , Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "support" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h2" } ) [] ) , TokenData [ ContentText "Support" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h2" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "Idris has been generously supported by the following " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://epsrc.ukri.org/" ] ] ) , TokenData [ ContentText "EPSRC" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText " grants:" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "ul" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "simple" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/N024222/1" ] ] ) , TokenData [ ContentText "Type-driven Verification of Communicating Systems" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1" ] ] ) , TokenData [ ContentText "Programming as Conversation: Type-Driven Development in Action" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "ul" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "We are also grateful for the continuing support of " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "reference external" ] , Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://www.sicsa.ac.uk/" ] ] ) , TokenData [ ContentText "SICSA" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText ", the Scottish Informatics and Computer Science Alliance" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "div" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "section" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "aside" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "sidebar" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "div" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "widget" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h2" } ) [] ) , TokenData [ ContentText "Categories" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h2" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "ul" } ) [] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/category/news.html" ] ] ) , TokenData [ ContentText "News" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "ul" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "div" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "div" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "widget social" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "h2" } ) [] ) , TokenData [ ContentText "Social" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "h2" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "ul" } ) [] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.idris-lang.org/feeds/all.atom.xml" ] , Attribute ( QName { namePrefix = "" , nameLocal = "rel" } ) [ ContentText "alternate" ] ] ) , TokenData [ ContentText "atom feed" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.twitter.com/idrislang" ] ] ) , TokenData [ ContentText "@idrislang" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "li" } ) [] ) , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://www.github.com/idris-lang" ] ] ) , TokenData [ ContentText "GitHub" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenEndTag ( QName { namePrefix = "" , nameLocal = "li" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "ul" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "div" } ) , TokenComment " /.social " , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "aside" } ) , TokenComment " /#sidebar " , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "footer" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "footer" ] , Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "body" ] ] ) , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "address" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "id" } ) [ ContentText "about" ] , Attribute ( QName { namePrefix = "" , nameLocal = "class" } ) [ ContentText "vcard body" ] ] ) , TokenData [ ContentText " Proudly powered by " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://alexis.notmyidea.org/pelican/" ] ] ) , TokenData [ ContentText "Pelican" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText ", which takes great advantage of " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "http://python.org" ] ] ) , TokenData [ ContentText "Python" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText " (not Idris :)). Patches are welcome on " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "a" } ) [ Attribute ( QName { namePrefix = "" , nameLocal = "href" } ) [ ContentText "https://github.com/edwinb/idris-lang.org/" ] ] ) , TokenData [ ContentText "github" ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "a" } ) , TokenData [ ContentText "! " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "address" } ) , TokenComment " /#about " , TokenData [ ContentText " " ] , TokenStartTag ( StartTag ( QName { namePrefix = "" , nameLocal = "p" } ) [] ) , TokenData [ ContentText "The theme is «notmyidea-cms», a modified version of «notmyidea», the default theme." ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "p" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "footer" } ) , TokenComment " /#footer " , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "body" } ) , TokenData [ ContentText " " ] , TokenEndTag ( QName { namePrefix = "" , nameLocal = "html" } ) , TokenData [ ContentText " " ] ]