From 2b7797235d69608e4221b287480949961aaa3948 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 Sep 2020 23:56:49 +0200 Subject: [PATCH] minor additions to standard library .... --- matita/matita/lib/lambda/etc/cons_r.etc | 7 +++++ .../lib/lambda/terms/supercombinator.ma | 27 +++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 matita/matita/lib/lambda/etc/cons_r.etc create mode 100644 matita/matita/lib/lambda/terms/supercombinator.ma diff --git a/matita/matita/lib/lambda/etc/cons_r.etc b/matita/matita/lib/lambda/etc/cons_r.etc new file mode 100644 index 000000000..46b2a08b7 --- /dev/null +++ b/matita/matita/lib/lambda/etc/cons_r.etc @@ -0,0 +1,7 @@ +notation "hvbox(l ⨭ break a)" + left associative with precedence 47 + for @{'cons_r $l $a}. + +interpretation "" 'nil = (Atom). + +interpretation "" 'cons_r tl hd = (tl hd). diff --git a/matita/matita/lib/lambda/terms/supercombinator.ma b/matita/matita/lib/lambda/terms/supercombinator.ma new file mode 100644 index 000000000..0f9279d79 --- /dev/null +++ b/matita/matita/lib/lambda/terms/supercombinator.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/terms/term.ma". + +(* SUPERCOMBINATOR **********************************************************) + +inductive is_supercombinator: nat → nat → predicate term ≝ +| is_supercombinator_vref: + ∀i,d. i < d → ∀h. is_supercombinator h d (#i) +| is_supercombinator_abst: + ∀A,h. is_supercombinator (S h) (S h) A → ∀d. is_supercombinator h d (𝛌.A) +| is_supercombinator_appl: + ∀B,A,d. is_supercombinator 0 d B → is_supercombinator 0 d A → + ∀h. is_supercombinator h d (@B.A) +. -- 2.39.2