MarcelineVQ

module Main

symbols : Stream Char
symbols = cycle (unpack "abc")

main : IO ()
main = do
    print $ take 10 symbols

MarcelineVQ

record OnsenM a where
  constructor MkOnsen
  runOnsen : (List String -> String, a)

emptyOnsenM : OnsenM ()

namespace AttribElem {
elem : String -> List Char -> OnsenM a -> OnsenM a
}
namespace Elem {

MarcelineVQ

data Tree : Type -> Type where
  Empty : Tree a
  MkTree : a -> List (Tree a) -> Tree a

total
map1 : (a -> b) -> Tree a -> Tree b
map1 f Empty = Empty
map1 f (MkTree x xs) = MkTree (f x) (map (map1 f) xs)

MarcelineVQ

data OpenSum (f :: k -> Type) (ts :: [k]) where
  UnsafeOpenSum :: Int -> f t -> OpenSum f ts

type FindElem (key :: k) (ts :: [k]) =
  FromMaybe Stuck =<< FindIndex (TyEq key) ts

type Member t ts = KnownNat (Eval (FindElem t ts))

findElem :: forall t ts. Member t ts => Int

MarcelineVQ

module Foo

data Singleton : (x : k) -> Type where
  With : (y : a) -> x = y -> Singleton x

inspect : (x : a) -> Singleton x
inspect x = With x Refl

all_values_filtered : (xs:List a) -> (f:a -> Bool) -> (all f (filter f xs) = True)
all_values_filtered [] f = Refl

MarcelineVQ

bool' : Bool -> a -> a -> a
bool' True x _ = x
bool' False _ y = y
  
filter' : (a -> Bool) -> List a -> List a
filter' f [] = []
filter' f (x :: xs) = bool' (f x) (x :: filter' f xs) (filter' f xs)

an : Bool -> Bool -> Bool
an True True = True

MarcelineVQ

data Foo : Nat -> Nat -> Type where
  Uuuh : Foo Z 0
  Aaah : Foo x y -> Foo x w -> Foo (S x) (y+w)

try_contradict : Foo n 0 -> (n = S Z) -> Void
try_contradict Uuuh Refl impossible
try_contradict (Aaah f g {y=Z} {w=Z} {x = Z}) prf = ?valid1
try_contradict (Aaah f g {y=Z} {w=Z} {x = (S k)}) prf = (\Refl impossible) prf
try_contradict (Aaah f g {y=Z} {w=S k}) prf impossible
try_contradict (Aaah f g {y=S j} {w=Z}) prf impossible

MarcelineVQ

data Foo : Nat -> Nat -> Type where
  Uuuh : Foo Z 0
  Aaah : Foo x y -> Foo x w -> Foo (S x) (y+w)

try_contradict : Foo n 0 -> IsSucc n -> Void
try_contradict Uuuh ItIsSucc impossible
try_contradict (Aaah f g {y=Z} {w=Z} {x = Z}) ItIsSucc = ?valid1
try_contradict (Aaah f g {y=Z} {w=Z} {x = (S k)}) ItIsSucc = ?valid2
try_contradict (Aaah f g {y=Z} {w=S k}) ItIsSucc  impossible
try_contradict (Aaah f g {y=S j} {w=Z}) ItIsSucc  impossible

MarcelineVQ

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Lib where

import Data.Char

MarcelineVQ

  ___
___ ___