Code Snippets Idris

Short texts Idris 🧑‍💻 Code snippets Idris ✍️ Reading lists Idris 👀

Incomplete example of DOM generation and interaction

module Web import Data.Vect import Data.Fuel import Data.String import Data.Nat import JS import Web.Dom import Web.Html import Nested edgeDescriptor : Edge -> String edgeDescriptor Vert = “vertical” edgeDescriptor Horiz = “horizontal” cornerDescriptor : Corner -> String cornerDescriptor TopLeft = “top-left” cornerDescriptor Bottomleft = “bottom-left” cornerDescriptor TopRight = “top-right” cornerDescriptor BottomRight = “bottom-right” classify : (t […]

Some code to give a feeling of proof-carrying code that uses `Ord`

module BST_Tornai import Data.So import Syntax.WithProof %default total infix 6 namespace WithExplicitPredicates_So — not so effective solution, but easier to be understood for liquidhaskellers, I think data BST : (a : Type) -> Ord a -> Type ( Bool (>>) : a -> BST a ord -> Bool data BST : (a : Type) -> […]

DPairQuoteProblem.idr

module DPairQuoteProblem import Language.Reflection %default total extract : Type -> Elab Unit extract ty = logTerm “debug.elab” 0 “type” !(quote ty) %macro extract’ : Type -> Elab Unit extract’ = extract — logTerm “debug.elab” 0 “type” !(quote ty) %language ElabReflection —————————– — One-parameter example — —————————– namespace OneParameter data Y : Nat -> Type where […]

dependent-mult-map.idr

%default total data Use = None | Once | Many %hide Prelude.Num.(*) %hide Prelude.Num.(+) %hide Prelude.List %hide Prelude.(::) %hide Prelude.Nil %hide Prelude.map %hide List.length %hide Prelude.Nat %hide Prelude.Z %hide Prelude.S %hide Builtin.fst (*) : Use -> Use -> Use Once * x = x Many * None = None Many * _ = Many None […]

Example of State Machine using Control.ST

import Data.Fuel import Control.ST %default total {-} Rewrite Vend.idr using Control.ST this example was useful for some parts https://github.com/owickstrom/fsm-your-compiler-wants-in/blob/master/src/listings/idris/Checkout.idr Improvements – better error messages (expected this state, but this is the actual state) – less boiler plate code (~100 lines less in this example) – better syntax for describing states A few things tricky things […]