File CoMoLang.Languages

Require Import List Logic.FinFun.

Set Implicit Arguments.

We need Logic.FinFun for a definition of finite Sets.

Print Finite.

A formal language is a subset of a finite alphabet, indicated by Pred.

Class Language (Sigma : Set) := {
    Pred : let word := list Sigma in word → Prop;
    Sigma_fin : Finite Sigma
    }
.

Section L_equiv.

  Variable Sigma : Set.

  Context `(L1 : Language Sigma).
  Context `(L2 : Language Sigma).

Two languages are equivalent, iff they accept the same words.