[isabelle] Value Parameter for Types

Dear All,

I am trying to put as much information as possible into the signature of my definitions.
Is it possible to give a value-parameter to a type?

For example the type of natural Numbers less or equal n:

typedef (n::nat) maxNat = "{i::nat | i. i≤n}"

n should be a parameter for the type. E.g. “5 maxNat” contains the elements 1…5.

This would be really fun, when (simple) operations like “+” can be used in the signature of definitions:

definition add::"n maxNat ⇒m maxNat ⇒(n+m) maxNat"

Thank you for the help,

Sebastian Stüber

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.