ckoparkar

 Elaborating Main.SplitView
 Cryptol.idr:83:6
 Main.SplitView pre-type {n : Nat} ->
(m : Nat) ->
Vect (mult m
n)
a ->
Type[]
 Main.SplitView type []
{a : _} ->

ckoparkar

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (succ n) with parity n
parity (succ .(k * 2)) | even k = odd k
parity (succ .(1 + k * 2)) | odd k = even (succ k)

ckoparkar

(define unops '(sub1 zero? car cdr))
(define binops '(* + > >= < <= = cons))

(define empty-env
  (lambda ()
    '(empty-env)))

(define extend-env
  (lambda (var val env)
    `(extend-env ,var ,val ,env)))

ckoparkar

To get around this, we have to prove that this recursion is "welll-founded". Consider the example of `<` and `<=`. The 
relation `<` is well-founded but `<=` is not. Because in `a < b < c`, we know that `a` is strictly less than `b`. This is 
finite and terminating. Whereas we can make infinite chains of `a <= a <= a ...`. This is called "accessibility". Using this 
concept, we have to prove that our `power` function is well-founded. I cannot fully explain this here; I am still working on 
understanding it completely. But this talk by Eric Mertens, https://vimeo.com/36519234 is really great. And here's a similar 
implementation in Idris, https://github.com/idris-lang/Idris dev/blob/0d3d2d66796b172e9933360aee51993a4abc624d/libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr.

ckoparkar

;; depends on monger
;; [com.novemberain/monger "3.1.0"]

(ns cider.nrepl.middleware.see-also
  (:require [monger.core :as mg]
            [monger.collection :as c]))

(defn extract-see-alsos
  []
  (let [conn (mg/connect)

ckoparkar

module Tree where

data Tree = Leaf Int | Node Int Tree Tree
  deriving (Show, Read, Eq, Ord)

type Forest = [Tree]

mkTree :: Int -> Tree
mkTree n =
  case n of

ckoparkar

module Blade where

import qualified Data.Set as S

-- Implemented the inclusion-exclusion algorithm:
-- <https://stackoverflow.com/a/27248971>

-- (∑ Aj) in the formula
-- These all the numbers we've counted more than once
doubleCounts :: [Int]

ckoparkar

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Bug where

{-

`rts.c` has a minimal RTS I'm using to test the object file linking. It houses the `main` function.
The main function calls `main_expr`, which is provided by this LLVM module. 

ckoparkar

Prog {ddefs = [("Tree",
                DDef {tyName = "Tree",
                      dataCons = [("Leaf", [(False, IntTy)]),
                                  ("Node",
                                   [(False, PackedTy "Tree" "loc92"),
                                    (False, PackedTy "Tree" "loc93")]),
                                  ("Node^",
                                   [(False, CursorTy),(False, PackedTy "Tree" "loc94"),
                                    (False, PackedTy "Tree" "loc95")]),
                                  ("INDIRECTION159", [(False, CursorTy)])]})],

ckoparkar

#include <assert.h>
#include <stdio.h>
// #include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <alloca.h>
#include <sys/mman.h>
#include <sys/resource.h>
#include <sys/stat.h>