[isabelle] Pattern Matching Problem
I need to define a function (say g) that involves non-constructor pattern
matching. Say S, C, and A are datatype constructors and f is a
function(f:: “a => nat”), I want to see if the argument of g matches with
the pattern “ S (C f(A 0))” or not, but it fails because f is not a
datatype constructor. How can I define such a function in HOL?
Any help would be appreciated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and