klauso

package test

import scala.language.higherKinds
import scala.language.implicitConversions

object CT {
    trait Category[Obj[_],C[_,_]] { // Obj is the value representation of objects, C the type representation of morphisms
        def id[A:Obj]: C[A,A]
        def compose[X:Obj,Y:Obj,Z:Obj](f: C[Y,Z], g: C[X,Y]): C[X,Z]
    }

klauso

package test

import scala.language.higherKinds

object CT {
    trait Category[Obj[_],C[_,_]] { // Obj is the value representation of objects, C the type representation of morphisms
        def id[A:Obj]: C[A,A]
        def compose[X:Obj,Y:Obj,Z:Obj](f: C[Y,Z], g: C[X,Y]): C[X,Z]
    }
    

klauso

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Either
import Control.Monad

klauso

module test where

open import Data.Nat
open import Data.Bool using (Bool; if_then_else_; true; false; _∧_)
open import Data.Product
import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq using (_≡_; refl; cong; sym)
open import Function.Equality using (_∘_)

klauso

module demo where


open import Data.Nat
open import Data.Bool using (Bool; if_then_else_; true; false; _∧_)
open import Data.Product
import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq using (_≡_; refl; cong; sym)
open import Function.Equality using (_∘_)

klauso

Class Litn Repr : Type := {
  litn : nat -> Repr;
}.

Class Litb Repr : Type := {
  litb : bool -> Repr;
}.

Class Add Repr : Type := {
  add : Repr -> Repr -> Repr

klauso

Require Import List.
Import ListNotations.
Require Import Coq.Arith.Arith.
Set Implicit Arguments.
Set Asymmetric Patterns.


Fixpoint lookup_simple {A} (pairs: list (nat * A)) (key :nat) : option (nat * A) := match pairs with
  | [] => None
  | a :: ss => if (beq_nat key (fst a))

klauso

Require Import List.
Import ListNotations.
Require Import Coq.Program.Basics. 

Set Implicit Arguments.

(******************)
(* standard hlist *)
(******************)