amutake

Require Import String List.
Import ListNotations.

Inductive Action : Type := action : string -> Action.

CoInductive Process : Type :=
| process : list (Action * Process) -> Process.

Inductive mu_derivative : Action -> Process -> Process -> Prop :=
| derivative_here : forall a q l, mu_derivative a (process ((a, q) :: l)) q

amutake

{-# LANGUAGE FlexibleContexts
  , TypeOperators
  , DeriveDataTypeable
  , ConstraintKinds
  , FlexibleInstances
  , MultiParamTypeClasses
  , UndecidableInstances #-}

import Control.Eff
import Control.Eff.Exception

amutake

Inductive A : Set := a : A.

Definition fantom (n : nat) := A.

Definition fantom_succ {n : nat} : fantom n -> fantom (S n) :=
  fun _ => a.

Inductive ty : forall n : nat, fantom n -> Prop :=
| zero : ty O a
| succ : forall (x : nat) (f : fantom x), ty x f -> ty (S x) (fantom_succ f).

amutake

-module(fizzbuzz).
-export([start/1]).

start(End) ->
    Pid = self(),
    FizzBuzz = spawn(fun() -> fizzbuzz(Pid, End) end),
    Fizz = spawn(fun() -> fizz(3) end),
    Buzz = spawn(fun() -> buzz(5) end),
    FizzBuzz ! {Fizz, Buzz},
    receive

amutake

module DeBruijn where

import Data.List

data Expr = Var Int | App Expr Expr | Abs Expr deriving (Eq, Show)

subst :: Expr -> Int -> Expr -> Expr
subst (Var n) m e
    | n == m = e
    | otherwise = Var n

amutake

module Main where

import Control.Applicative ((<$>))
import Control.Monad (forM)

type Pos = (Int, Int)

main :: IO ()
main = do
    n <- read <$> getLine

amutake

test

# test2

main = putStrLn "helloworld"

amutake

import Control.Applicative
import Control.Monad
import Data.List

main = do
    [m, n] <- map read . words <$> getLine
    s <- forM [1..m] (\x -> getLine)
    putStrLn $ show $ s !! n