From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 25 Sep 2020 21:56:49 +0000 (+0200)
Subject: minor additions to standard library
X-Git-Tag: make_still_working~176
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2b7797235d69608e4221b287480949961aaa3948

minor additions to standard library

....
---

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)
+.