[isabelle] parameters of function definitions and scope of constants
Thnx for the answers to my previous questions. I have 2 more :)
1) When defining a function using the `fun' keyword, it is not possible
to use the name of an existing constant as parameter. E.g.,
definition foo :: "bool" where "foo = True"
fun bar :: "nat => nat" where "bar foo = Suc(foo)"
doesn't work. It produces:
*** Type unification failed: Clash of types "bool" and "nat"
*** Type error in application: Incompatible operand type
*** Operator: bar :: nat => nat
*** Operand: foo :: bool
*** At command "fun".
Is that the intended behavior?
2) Is it possible to `hide' previously defined constants that have only
be used in some lemmas and aren't needed later on, in order to be able
to reuse the name? Or put differently, can I use `fun' and/or
`definition' in a local scope (let's say, within a proof)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and