Library CoLoR.Term.SimpleType.TermsSig

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.

Adam Koprowski, 2006-04-27

This file presents the definition of simple types for the development of theory of simpe typed lambda-calculus.

Set Implicit Arguments.

Module Type BaseTypes.

  Parameter BaseType : Type.
  Implicit Types a b c : BaseType.
  Parameter eq_BaseType_dec : ∀ (a b: BaseType), {a =b }+{¬a =b }.
  Hint Resolve eq_BaseType_dec : terms.
  Parameter baseTypesNotEmpty : BaseType.

End BaseTypes.

Module SimpleTypes (BT : BaseTypes).

  Export BT.

  Inductive SimpleType : Type :=
    | BasicType(T: BaseType)
    | ArrowType(A B : SimpleType).
  Notation "x --> y" := (ArrowType x y)
    (at level 55, right associativity) : type_scope.
  Notation "# x " := (BasicType x) (at level 0) : type_scope.
  Implicit Types A B C : SimpleType.
  Hint Constructors SimpleType : terms.

End SimpleTypes.

Module Type Signature.

  Declare Module BT : BaseTypes.
  Module ST := SimpleTypes BT.
  Import ST.
  Export ST.

  Parameter FunctionSymbol : Type.
  Implicit Types f g h : FunctionSymbol.

  Parameter eq_FunctionSymbol_dec : ∀ (f g: FunctionSymbol),
    {f =g } + {¬f =g }.
  Hint Resolve eq_FunctionSymbol_dec : terms.

  Parameter functionSymbolsNotEmpty : FunctionSymbol.

  Parameter f_type : FunctionSymbol → SimpleType.

End Signature.