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 : forall (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 Export ST := SimpleTypes BT.

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

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

  Parameter functionSymbolsNotEmpty : FunctionSymbol.

  Parameter f_type : FunctionSymbol -> SimpleType.

End Signature.