archaeron

let optionize f = 
    function
    | None -> None
    | Some(x) -> Some(f x)

let newListMap f list = List.map (optionize f) list

let listWithNull = [Some 0; Some 6; Some 3; None; Some 34; None; Some 1]

let square x = x*x

archaeron

class Monoid
	mempty: ->
		throw new Error "mempty not implemented"
	mappend: ->
		throw new Error "mappend not implemented"
	mconcat: ->
		throw new Error "mconcat not implemented"

class Option extends Monoid
	mempty: ->

archaeron

000473(:return (:ok "Data type Nat : Type
    Unary natural numbers
    
Constructors:
    Z : Nat
        Zero
        
    S : Nat -> Nat
        Successor
        " ((10 3 ((:name "Prelude.Nat.Nat") (:implicit :False) (:decor :type) (:doc-overview "Unary natural numbers") (:type "Type") (:namespace "Prelude.Nat"))) (16 4 ((:decor :type) (:type "Type") (:doc-overview "The type of types") (:name "Type"))) (70 1 ((:name "Prelude.Nat.Z") (:implicit :False) (:decor :data) (:doc-overview "Zero") (:type "Nat") (:namespace "Prelude.Nat"))) (74 3 ((:name "Prelude.Nat.Nat") (:implicit :False) (:decor :type) (:doc-overview "Unary natural numbers") (:type "Type") (:namespace "Prelude.Nat"))) (104 1 ((:name "Prelude.Nat.S") (:implicit :False) (:decor :data) (:doc-overview "Successor") (:type "Nat -> Nat") (:namespace "Prelude.Nat"))) (108 3 ((:name "Prelude.Nat.Nat") (:implicit :False) (:decor :type) (:doc-overview "Unary natural numbers") (:type "Type") (:namespace "Prelude.Nat"))) (115 3 ((:name "Prelude.Nat.Nat") (:

archaeron

module Test

a

archaeron

module Main

import Data.Vect

main : IO ()
main = putStrLn "Hello world\n\o44\5\xa4"

zipWithF : (a -> b -> c) -> List a -> List b -> List c
zipWithF f xs ys = ?zipWithF_rhs_2

archaeron

module Test

a : (String -> Either String String) -> String
a b =
	case b of
		Left err => err
		Right v => v

archaeron

((((:filename ".\\Highlight\\Main.idr") (:start 1 8) (:end 1 22)) ((:namespace "Highlight.Main") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\idris-code-highlighter\\src\\Highlight\\Main.idr"))) (((:filename ".\\Highlight\\Parser.idr") (:start 1 8) (:end 1 24)) ((:namespace "Highlight.Parser") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\idris-code-highlighter\\src\\Highlight\\Parser.idr"))) (((:filename ".\\Highlight\\Regions.idr") (:start 1 8) (:end 1 25)) ((:namespace "Highlight.Regions") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\idris-code-highlighter\\src\\Highlight\\Regions.idr"))) (((:filename ".\\Highlight\\Regions.idr") (:start 1 8) (:end 1 25)) ((:namespace "Highlight.Regions") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\idris-code-highlighter\\src\\Highlight\\Regions.idr"))) (((:filename ".\\Highlight\\Formats.idr") (:start 1 8) (:end 1 25)) ((:

archaeron

Keybase proof

I hereby claim:

• I am archaeron on github.
• I am archaeron (https://keybase.io/archaeron) on keybase.
• I have a public key ASCMJritEyCIwn247mMKQGggmI1uINWwo7qI8QMYtHCFUgo

To claim this, I am signing this object:

archaeron

with import <nixpkgs> {};

let
  ocamlPackages = pkgs.recurseIntoAttrs pkgs.ocamlPackages_4_03;
  ocamlVersion = (builtins.parseDrvName ocamlPackages.ocaml.name).version;
  findlibSiteLib = "${ocamlPackages.findlib}/lib/ocaml/${ocamlVersion}/site-lib";
  ocamlInit = pkgs.writeText "ocamlinit" ''
    let () =
      try Topdirs.dir_directory "${findlibSiteLib}"
      with Not_found -> ()

archaeron

1. stack2nix . > nix/stack.nix
2. nix-shell default.nix -A api