tanakh

{-# LANGUAGE DeriveFunctor, TypeFamilies, EmptyDataDecls, PolyKinds, DataKinds, ConstraintKinds #-}

newtype Dimensional (dim :: Dimension) a = Dimensional a
  deriving (Eq, Ord, Show, Functor)

data Dimension = Dim0 | Dim String Int Dimension

type family Insert (a :: Dimension) (k :: String) (v :: Int) :: Dimension
type instance Insert (Dim0 k v) = Dim k v Dim0
type instance (k < a) => Insert (Dim a b l) k v = Dim k v (Dim a b l)

tanakh

{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes           #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

import           Control.Lens                 hiding (Rep, from, to)

tanakh

module Foo (
  module Bar,
  module Baz,
  ...
  ) where

import Bar
import Baz
...

tanakh

import Control.Applicative
import Control.Monad
import Data.Char
import Data.List.Split
import Data.SBV

main :: IO ()
main = do
  t <- map read . words <$> getLine
  case t of

tanakh

import Data.SBV

godNumber :: Int
godNumber = 50

p1 :: [[SInteger]]
p1 =
  [ [11, 2, 8, 5]
  , [13, 14, 10, 12]
  , [4, 3, 1, 7]

tanakh

#include <vcc.h>

_(logic \bool sorted(int *buf, unsigned len) =
  \forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j])

_(logic \bool is_minimum(int *buf, unsigned l, unsigned r, unsigned x) =
  \forall unsigned i; l <= i && i < r ==> buf[x] <= buf[i])

unsigned find_min(int *v, unsigned l, unsigned r)
  _(requires \thread_local_array(v, r))

tanakh

#include <vcc.h>

_(logic \bool sorted(int *buf, unsigned len) =
  \forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j])

_(typedef unsigned perm_t[unsigned];)

_(logic \bool is_permutation(perm_t perm, unsigned len) =
  (\forall unsigned i, j;
    i < j && j < len ==> perm[i] != perm[j]))

tanakh

theory Scratch
imports Main
begin

primrec ins :: "int => int list => int list" where
  "ins x [] = [x]" |
  "ins x (y # ys) = (if x <= y then (x # y # ys) else (y # ins x ys))"

primrec sort :: "int list => int list" where
  "sort [] = []" |

tanakh

theory Sorts
imports Main
begin

primrec insert :: "int => int list => int list" where
  "insert v [] = [v]" |
  "insert v (x # xs) =
    (if v <= x then v # x # xs else x # insert v xs)"

primrec insert_sort :: "int list => int list" where

tanakh

{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}

module Sorts where {

import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
  String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;