canonic-epicure

type Effect = { kind : string }
type EffectHandler<E extends Effect> = (e : E) => unknown

function runGeneratorSyncWithEffect<ResultT, YieldT extends Effect, ArgsT extends any[]> (
    effectHandler   : EffectHandler<YieldT>,
    func            : (...args : ArgsT) => Generator<YieldT, ResultT, any>,
    args            : ArgsT,
    scope?          : any
) : ResultT
{

canonic-epicure

module Exprm_FunctionImage where

open import Data.Vec
open import Data.List

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

module FunctionImage where
    data FunctionImage1 : {A B : Set} -> (f : A -> B) -> A -> B -> Set where

canonic-epicure

data Action = Flower | Upwards | Branch

data RndGen

RndNumGen : Type
RndNumGen = EffM Identity Action [RND] (const [RND])

getRnd : RndNumGen -> (Action, RndNumGen)
getRnd prev =
    let

canonic-epicure

module Language

import Data.So

%default total

record SomeRec where
    constructor MkSomeRec

    WhereCondition  : Bool

canonic-epicure

module Language

import Data.So

%default total

-- typechecks after removing "mutual"
mutual
    record SomeRec where
        constructor MkSomeRec

canonic-epicure

module SQL where

open import Data.Nat

a : Nat
a = 1


{- 

canonic-epicure

module SQL

%default total
%access public export

data SqlType = BOOLEAN | INTEGER

mutual
    data ColumnExpression : SqlType -> Type where
        BooleanLiteral  : Bool -> ColumnExpression BOOLEAN

canonic-epicure

module Algebra

data ExprF : (carrier : Type) -> Type where
    Const       : Int -> ExprF carrier
    Add         : (a : carrier) -> (b : carrier) -> ExprF carrier
    Mul         : (a : carrier) -> (b : carrier) -> ExprF carrier


data Fix : (f : Type -> Type) -> Type where
    In : f (Fix f) -> Fix f

canonic-epicure

module Language

%default total

mutual
    data QuerySource : Type where
        Table           : (tableName : String) -> QuerySource
        SubQuery        : Bool -> QuerySource
        As              : (source : QuerySource) -> {auto prf : QuerySourceIsNotAliased source} -> (aliasName : String) -> QuerySource

canonic-epicure

module Language

import Control.Monad.State

%default total

%access public export

mutual
    record QueryAbstractSyntaxTree where