Library CoLoR.Term.SimpleType.TermsSig
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
This file presents the definition of simple types
for the development of theory of simpe typed lambda-calculus.
- Adam Koprowski, 2006-04-27
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.