Please note that there is a file "lambdapi.pkg" at the same level of this directory's content. This file is composed of the following lines:

package_name = AL_library
root_path = AL_library

Content of files :

• (number).lp: linking with the issue n°(number)

• Notation.lp: general notations : Proposition type + Set type + Leibniz equality

• Constructive_logic.lp: Constructive logic rules on conjunction, disjunction, false, true, negation, implication, equivalence, universal quantification, existential quantification

• Classical_logic.lp: Classical logic rules (extension of Constructive_logic.lp)

• Logic_lemma.lp: Some lemmas about logic

• Bool.lp: definition of type + induction principle + not or {|and|} + some examples of functions

• Bool_lemma.lp: some easy lemmas

• Bool_list.lp: some easy things about boolean lists

• Nat.lp : definition of type + lemmas about natural numbers

• Operations.lp : eqb_nat/leb_nat/ltb_nat + lemmas about these operations

• Discriminate.lp: my job about the tactic discriminate

• Non-recursive_type.lp: A simple example of inductive type

• Color.lp: A simple example of induction

• Bag_via_list.lp: Definition of polymorphic IF

• Polymorphic_list.lp: definition and lemmas about polymorphic lists

• Even.lp: Definition of a first inductive predicat

• tp_dubois_pfm.lp: a saving