rodrigogribeiro

Set Implicit Arguments.

Require Import Arith List.

Definition name := nat

(***********************************************************************)
(** Definition of types.                                              **)

Inductive ty : Set :=

rodrigogribeiro

Set Implicit Arguments.

Require Import Recdef List.

Require Import LibTactics.
Require Import TyOrder Subst Ty Monad Arith_base.

Include SUBST.
Include TYORDER.

rodrigogribeiro

module Preliminaries where

-- levels

postulate Level : Set
postulate LZero : Level
postulate LSuc  : Level -> Level
postulate LMax  : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}

rodrigogribeiro

module Preliminaries where

-- levels

postulate Level : Set
postulate LZero : Level
postulate LSuc  : Level -> Level
postulate LMax  : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}

rodrigogribeiro

module Preliminaries where

-- levels

postulate Level : Set
postulate LZero : Level
postulate LSuc  : Level -> Level
postulate LMax  : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}

rodrigogribeiro

Set Implicit Arguments.

Require Import Arith.Arith_base List Omega.
Require Import Wellfounded.Lexicographic_Product.
Require Import Relation_Operators.
Require Import JMeq.

(* Notation for heterogeneous equality *)

Infix "==" := JMeq (at level 70, no associativity).

rodrigogribeiro

Inductive Kind : Set :=
  | Star : Kind
  | KFun : Kind -> Kind -> Kind.

Definition eq_kind_dec : forall (k k' : Kind), {k = k'} + {k <> k'}.
  decide equality.
Defined.

Notation ":*" := Star.
Notation "k '==>' k'" := (KFun k k') (at level 60, right associativity).

rodrigogribeiro

open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Nat renaming (ℕ to Nat)
open import Data.Product
open import Data.Vec using (Vec ; lookup)
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_ ; sym to symm)

module Test (A : Set)(fail : A) where

rodrigogribeiro

module RegExp

%default total

data RegExp : Type where
  Zero : RegExp
  Eps  : RegExp  
  Chr  : Char -> RegExp
  Cat  : RegExp -> RegExp -> RegExp
  Alt  : RegExp -> RegExp -> RegExp

rodrigogribeiro

module RegExp

%default total

data RegExp : Type where
  Zero : RegExp
  Eps  : RegExp  
  Chr  : Char -> RegExp
  Cat  : RegExp -> RegExp -> RegExp
  Alt  : RegExp -> RegExp -> RegExp