2013 | split_lambda (Const ("Pair", _) $ t1 $ t2) t = |
2013 | split_lambda (Const ("Pair", _) $ t1 $ t2) t = |
2014 HOLogic.mk_split (split_lambda t1 (split_lambda t2 t)) |
2014 HOLogic.mk_split (split_lambda t1 (split_lambda t2 t)) |
2015 | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t) |
2015 | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t) |
2016 | split_lambda t _ = raise (TERM ("split_lambda", [t])) |
2016 | split_lambda t _ = raise (TERM ("split_lambda", [t])) |
2017 |
2017 |
2018 fun strip_split_abs (Const ("split", _) $ t) = strip_split_abs t |
2018 fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t |
2019 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t |
2019 | strip_split_abs (Abs (_, _, t)) = strip_split_abs t |
2020 | strip_split_abs t = t |
2020 | strip_split_abs t = t |
2021 |
2021 |
2022 fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names = |
2022 fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names = |
2023 if eq_mode (m, Input) orelse eq_mode (m, Output) then |
2023 if eq_mode (m, Input) orelse eq_mode (m, Output) then |