(**************************************************************************) (* ___ *) (* ||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 *) (* *) (**************************************************************************) (* MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1): MATITA SOURCE FILES * Specification started: 2011 December 12 * - Patience on me to gain peace and perfection! - *) include "basic_2/grammar/lenv.ma". include "apps_2/MLTT1_1/notation.ma". (* EXTENDED NOTATION ********************************************************) definition sort ≝ 0. interpretation "global definition" 'LAbbr L T = (LPair L Abbr T). interpretation "global declaration" 'LAbst L T = (LPair L Abst T). interpretation "atom (arity)" 'Box = (TAtom (Sort sort)). interpretation "function (arity)" 'TImp T1 T2 = (TPair Abst T1 T2). interpretation "function (term)" 'TAbst T = (TPair Abst (TAtom (Sort sort)) T).