gaxiiiiiiiiiiii

Require Import Nat.
Require Import Arith.
Require Import Lia.
Require Import Wf.


Inductive term :=
    | t_true : term 
    | t_false : term 

gaxiiiiiiiiiiii

Require Import ssreflect.
Require Import Nat Arith.


Definition id := nat.

Inductive type : Type :=
    | Bool : type 
    | Nat : type

gaxiiiiiiiiiiii

From mathcomp Require Import ssrbool ssrnat.

Section Eden.

(********************)
(* Primitive states *)
(********************)


Variable Subject : Type.

gaxiiiiiiiiiiii

Require Import RelationClasses Relation_Definitions Morphisms.




Class Graph := {
    T : Type;
    X : T -> T -> Type;
    equal : forall n m, relation (X n m); (* X -> X -> Prop from Relation_Definitions*)

gaxiiiiiiiiiiii

Require Export Lib.

(*
Inductive id : Type :=
    Id : nat -> id.
*)


Inductive type : Type :=
    | BOOL : type

gaxiiiiiiiiiiii

Inductive peano : Set :=
    | Z : peano
    | S : peano -> peano.


Inductive Plus : peano -> peano -> peano -> Prop :=
    | P_Zero : forall n, Plus Z n n
    | P_Succ : forall n m l,
                Plus n m l -> Plus (S n) m (S l).

gaxiiiiiiiiiiii

import Data.List
import Control.Monad
import Control.Concurrent
import System.Random.Shuffle (shuffleM)


------------------------------
-- Comonad
------------------------------
class Functor w => Comonad w where

gaxiiiiiiiiiiii

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}

module StackMachine where

import Control.Monad.Free
import Control.Monad.Trans.State
import Prelude hiding (EQ, LT, GT)

gaxiiiiiiiiiiii

{-# LANGUAGE FlexibleInstances #-}
module ControllerDSL where

import Control.Monad.Free
import qualified Control.Monad.State as S (liftIO)
import qualified Control.Monad.Trans.State as S
import Prelude hiding (read)
import qualified Data.Map as M

-- These types are defined in a separate library

gaxiiiiiiiiiiii

module BlackJack where

import Control.Monad (liftM2)    
import Data.Char (toLower)
import Data.List (intercalate, sort)
import System.Random.Shuffle (shuffleM)
import Control.Monad (sequence)
import Control.Monad.Trans.State 
import Control.Monad.Trans.Class
import Control.Monad.Trans.Except