# HG changeset patch
# User wenzelm
# Date 1629922587 -7200
# Node ID 1f78a40e439920ea8021f81f3ac20ee024cdb68a
# Parent  6dc7ff3269065089dcd7bbef2448dbcb752e02dd
more Isabelle/Haskell operations;

diff -r 6dc7ff326906 -r 1f78a40e4399 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Aug 25 17:46:53 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed Aug 25 22:16:27 2021 +0200
@@ -2229,7 +2229,7 @@
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
   Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
-  type_op0, type_op1, op0, op1, op2, typed_op1, typed_op2, binder,
+  type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
 )
@@ -2363,6 +2363,13 @@
     dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
     dest _ = Nothing
 
+typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ)
+typed_op0 name = (mk, dest)
+  where
+    mk ty = Const (name, [ty])
+    dest (Const (c, [ty])) | c == name = Just ty
+    dest _ = Nothing
+
 typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
 typed_op1 name = (mk, dest)
   where
@@ -2479,7 +2486,8 @@
   mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
   mk_imp, dest_imp, mk_iff, dest_iff,
   mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
-  mk_all, dest_all, mk_ex, dest_ex
+  mk_all, dest_all, mk_ex, dest_ex,
+  mk_undefined, dest_undefined
 )
 where
 
@@ -2540,6 +2548,9 @@
 
 mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>
+
+mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ
+(mk_undefined, dest_undefined) = typed_op0 \<open>\<^const_name>\<open>undefined\<close>\<close>
 \<close>
 
 generate_file "Isabelle/Term_XML/Encode.hs" = \<open>