text:
Lean Tutorial
=============

Introduction
------------

Lean is an automatic and interactive theorem prover. It can be used to
create specifications, build mathematical libraries, and solve
constraints. In this tutorial, we introduce basic concepts, the logic
used in Lean, and the main commands.

Getting started
---------------

We can use Lean in interactive or batch mode.
The following example just displays the message `hello world`.

```lean
        print "hello world"
```

All we have to do to run your first example is to call the `lean` executable
with the name of the text file that contains the command above.
If you saved the above command in the file `hello.lean`, then you just have
to execute

       lean hello.lean

As a more complex example, the next example defines a function that doubles
the input value.

```lean
      -- defines the double function
      definition double (x : Nat) := x + x
```

Basics
------

We can also view Lean as a suite of tools for evaluating and processing
expressions representing terms, definitions, and theorems.

Every expression has a unique type in Lean. The command `check` returns the
type of a given expression.

```lean
      check double 3
      check double
```

The last command returns `Nat → Nat`. That is, the type of double is a function
from `Nat` to `Nat`, where `Nat` is the type of the natural numbers.

The command `import` loads existing libraries and extensions. The
following command imports the command `find` that searches the Lean
environment using regular expressions

```lean
      import find

      find "Nat"      -- find all object that start with the prefix Nat
      check Nat::ge   -- display the signature of the Nat::ge definition
```

We say `Nat::ge` is a hierarchical name comprised of two parts: `Nat` and `ge`

The command `using` creates aliases based on a given prefix. For example, the following
command creates aliases for all objects starting with `Nat`

```lean
      using Nat
      check ge       -- display the signature of the Nat::ge definition
```

The command `variable` assigns a type to an identifier. The following command postulates/assumes
that `n`, `m` and `o` have type `Nat`.

```lean
      variable n : Nat
      variable m : Nat
      variable o : Nat
```

The command `variables n m o : Nat` can be used a shorthand for the three commands above.

In Lean, proofs are also expressions, and all functionality provided for manipulating
expressions is also available for manipulating proofs. For example, `refl n` is a proof
for `n = n`. In Lean, `refl` is the reflexivity theorem.

```lean
     check refl n
```

The command `axiom` postulates that a given proposition (aka Boolean formula) is true.
The following commands postulate two axioms `Ax1` and `Ax2` that state that `n = m` and
`m = o`.

```lean
      axiom Ax1 : n = m
      axiom Ax2 : m = o
```

`Ax1` and `Ax2` are not just names. For example, `trans Ax1 Ax2` is a proof that
`n = o`, where `trans` is the transitivity theorem.

```lean
      check trans Ax1 Ax2
```

The expression `trans Ax1 Ax2` is just a function application like any other.
Moreover, in Lean, _propositions are types_. Any Boolean expression `P` can be used
as a type. The elements of type `P` can be viewed as the proofs of `P`.
Moreover, in Lean, _proof checking is type checking_. For example, the Lean type checker
will reject the type incorrect term `trans Ax2 Ax1`.

Because we use _proposition as types_, we must support _empty types_. For example,
the type `false` must be empty, since we don't have a proof for `false`.

Most systems based on the _propositions as types_ paradigm are based on constructive logic.
Lean on the other hand is based on classical logic. The _excluded middle_ is a theorem
in Lean, and `em p` is a proof for `p ∨ ¬ p`.

```lean
    variable p : Bool
    check em p
```

The commands `axiom` and `variable` are essentially the same command. We provide both
just to make Lean files more readable. We encourage users to use `axiom` only for
propostions, and `variable` for everything else.

Similarly, a theorem is just a definition. The following command defines a new theorem
called `nat_trans3`

```lean
      theorem nat_trans3 (a b c d : Nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
      := trans (trans H1 (symm H2)) H3
```

The theorem `nat_trans3` has 7 parameters, it takes for natural numbers `a`, `b`, `c` and `d`,
and three proofs showing that `a = b`, `c = b` and `c = d`, and returns a proof that `a = d`.
In the example above, `symm` is the symmetry theorem. Now, we use `nat_trans3` in a simple
example.

```lean
      variables x y z w : Nat
      axiom Hxy : x = y
      axiom Hzy : z = y
      axiom Hzw : z = w
      check nat_trans3 x y z w Hxy Hzy Hzw
```

The theorem `nat_trans3` is somewhat inconvenient to use because it has 7 parameters.
However, the first four parameters can be inferred from the last 3. We can use `_` as a placeholder
that instructs Lean to synthesize this expression. The synthesis process is based on type inference, and it is
the most basic form of automation provided by Lean.

```lean
      check nat_trans3 _ _ _ _ Hxy Hzy Hzw
```

Lean also supports _implicit arguments_.
We mark implicit arguments using curly braces instead of parenthesis.
In the following example, we define the theorem `nat_trans3i` using implicit arguments.

```lean
      theorem nat_trans3i {a b c d : Nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
      := trans (trans H1 (symm H2)) H3
```

It is identical to `nat_trans3`, the only difference is the use of curly braces.
Lean will (try to) infer the implicit arguments. The idea behind implicit arguments
is quite simple, we are just instructing Lean to automatically insert the placeholders
`_` for us.

```lean
      check nat_trans3i Hxy Hzy Hzw
```

Sometimes, Lean will not be able to infer the parameters automatically.
So, whenever we define a theorem/definition/axiom/variable containing implicit arguments, Lean will
automatically create an _explicit_ version where all parameters are explicit.
The explicit version uses the same name with a `@` prefix.

```lean
      check @nat_trans3i
```

The theorems `refl`, `trans` and `symm` all have implicit arguments.

```lean
      check @refl
      check @trans
      check @symm
```

We can also instruct Lean to display all implicit arguments when it prints expressions.
This is useful when debugging non-trivial problems.

```lean
      set_option pp::implicit true   -- show implicit arguments
      check nat_trans3i Hxy Hzy Hzw
      set_option pp::implicit false  -- hide implicit arguments
```

In the previous example, the `check` command stated that `nat_trans3i Hxy Hzy Hzw`
has type `@eq ℕ x w`. The expression `x = w` is just notational convenience.

We have seen many occurrences of `(Type U)`, where `U` is a _universe variable_.
In Lean, the type of `Nat` and `Bool` is `Type`.

```lean
      check Nat
      check Bool
```

We say `Type` is the type of all _small_ types, but what is the type of `Type`?

```lean
      check Type
```

Lean returns `(Type 1)`. Similarly, the type of `(Type 1)` is `(Type 2)`. In Lean, we also have _universe cumulativity_.
That is, we can provide an element of type `(Type i)` where an element of type `(Type j)` is expected when `i ≤ j`.
This makes the system more convenient to use. Otherwise, we would need a reflexivity theorem for `Type` (i.e., `(Type 0)`),
`Type 1`, `Type 2`, etc. Universe cumulativity improves usability, but it is not enough because
we would still have the question: how big should `i` be? Moreover, if we choose an `i` that is not big enough
we have to go back and correct all libraries. This is not satisfactory and not modular.
So, in Lean, we allow users to declare _universe variables_ and simple constraints between them. The Lean kernel defines
one universe variable `U`, and states that `U ≥ 1` using the command `universe U ≥ 1`.
The Lean type casting library defines another universe variable called `M` and states that `universe M ≥ 1`.
In Lean, whenever we declare a new universe `V`, the system automatically adds the constraint `U ≥ V + 1`.
That is, `U` the _maximal_ universe in Lean.
Lean reports an universe inconsistency if the universe constraints are inconsistent. For example, it will return an error
if execute the command `universe M ≥ U`. We can view universe variables as placeholders, and we can always solve
the universe constraints and find and assignment for the universe variables used in our developments.
This assignment allows us to automatically generate a Lean specification that is not based on this particular feature.

Propositional logic
-------------------

To manipulate formulas with a richer logical structure, it is important to master the notation Lean uses for building
composite logical expressions out of basic formulas using _logical connectives_. The logical connectives (`and`, `or`, `not`, etc)
are defined in the Lean [kernel](../../src/builtin/kernel.lean). The kernel also defines notational convention for rewriting formulas
in a natural way. Here is a table showing the notation for the so called propositional (or Boolean) connectives.

| Ascii | Ascii alt.  | Unicode  | Definition  |
|-------|--------------|---------|--------------|
| true  |              | ⊤       |   true       |
| false |              | ⊥       |   false      |
| not   |              | ¬       |   not        |
| /\    | &&           | ∧       |   and        |
| \/    | || | ∨       |   or         |
| ->    |              | →      |  implies     |
| <->   |              | ↔       |  iff         |

`true` and `false` are logical constants to denote the true and false propositions. Logical negation is a unary operator just like
arithmetical negation on numbers. The other connectives are all binary operators. The meaning of the operators is the usual one.
The table above makes clear that Lean supports unicode characters. We can use Ascii or/and unicode versions.
Here is a simple example using the connectives above.

```lean
    variable q : Bool
    check p → q → p ∧ q
    check ¬ p → p ↔ false
    check p ∨ q → q ∨ p
    -- Ascii version
    check p -> q -> p && q
    check not p -> p <-> false
    check p || q -> q \/ p
```

Depending on the platform, Lean uses unicode characters by default when printing expressions. The following commands can be used to
change this behavior.

```lean
    set_option pp::unicode false
    check p → q → p ∧ q
    set_option pp::unicode true
    check p → q → p ∧ q
```

Note that, it may seem that the symbols `->` and `→` are overloaded, and Lean uses them to represent Boolean implication and the type
of functions. Actually, they are not overloaded, they are the same symbols. In Lean, the Boolean `p → q` expression is also the type
of the functions that given a proof for `p`, returns a proof for `q`. This is very convenient for writing proofs.

```lean
   -- Hpq is a function that takes a proof for p and returns a proof for q
   axiom Hpq : p → q
   -- Hq is a proof/certificate for p
   axiom Hp  : p
   -- The expression Hpq Hp is a proof/certificate for q
   check Hpq Hp
```

In composite expressions, the precedences of the various binary
connectives are in order of the above table, with `and` being the
strongest and `iff` the weakest. For example, `a ∧ b → c ∨ d ∧ e`
means `(a ∧ b) → (c ∨ (d ∧ e))`. All of them are right-associative.
So, `p ∧ q ∧ r` means `p ∧ (q ∧ r)`. The actual precedence and fixity of all
logical connectives is defined in the Lean [kernel definition file](../../src/builtin/kernel.lean).

Finally, `not`, `and`, `or` and `iff` are the actual names used when
defining the Boolean connectives. They can be used as any other function.

```lean
   check and
   check or
   check not
```

Lean supports _currying_ `and true` is a function from `Bool` to `Bool`.

```lean
   check and true
   definition id := and true
```

Functions
---------

There are many variable-binding constructs in mathematics. Lean expresses
all of them using just one _abstraction_, which is a converse operation to
function application. Given a variable `x`, a type `A`, and a term `t` that
may or may not contain `x`, one can construct the so-called _lambda abstraction_
`fun x : A, t`, or using unicode notation `λ x : A, t`. Here is some simple
examples.

```lean
   check fun x : Nat, x + 1
   check fun x y : Nat, x + 2 * y
   check fun x y : Bool, not (x ∧ y)
   check λ x : Nat, x + 1
   check λ (x : Nat) (p : Bool), x = 0 ∨ p
```

In many cases, Lean can automatically infer the type of the variable. Actually,
In all examples above, the type can be inferred automatically.

```lean
   check fun x, x + 1
   check fun x y, x + 2 * y
   check fun x y, not (x ∧ y)
   check λ x, x + 1
   check λ x p, x = 0 ∨ p
```

However, Lean will complain that it cannot infer the type of the
variable `x` in `fun x, x` because any type would work in this example.

The following example shows how to use lambda abstractions in
function applications

```lean
   check (fun x y, x + 2 * y) 1
   check (fun x y, x + 2 * y) 1 2
   check (fun x y, not (x ∧ y)) true false
```

Lambda abstractions are also used to create proofs for propositions of the form `A → B`.
This should be natural since we can "view" `A → B` as the type of functions that given
a proof for `A` returns a proof for `B`.
For example, a proof for `p → p` is just `fun H : p, H` (the identity function).

```lean
    check fun H : p, H
```

Definitional equality
---------------------

The command `eval t` computes a normal form for the term `t`.
In Lean, we say two terms are _definitionally equal_ if the have the same
normal form. For example, the terms `(λ x : Nat, x + 1) a` and `a + 1`
are definitionally equal. The Lean type/proof checker uses the normalizer when
checking types/proofs. So, we can prove that two definitionally equal terms
are equal using just `refl`. Here is a simple example.

```lean
   theorem def_eq_th (a : Nat) : ((λ x : Nat, x + 1) a) = a + 1
   := refl (a+1)
```

Provable equality
-----------------

In the previous examples, we have used `nat_trans3 x y z w Hxy Hzy Hzw`
to show that `x = w`. In this case, `x` and `w` are not definitionally equal,
but they are provably equal in the environment that contains `nat_trans3` and
axioms `Hxy`, `Hzy` and `Hzw`.

Proving
-------

The Lean kernel contains basic theorems for creating proof terms.  The
basic theorems are useful for creating manual proofs. The are also the
basic building blocks used by all automated proof engines available in
Lean. The theorems can be broken into three different categories:
introduction, elimination, and rewriting. First, we cover the introduction
and elimination theorems for the basic Boolean connectives.

### And (conjuction)

The expression `and_intro H1 H2` creates a proof for `a ∧ b` using proofs
`H1 : a` and `H2 : b`. We say `and_intro` is the _and-introduction_ operation.
In the following example we use `and_intro` for creating a proof for
`p → q → p ∧ q`.

```lean
   check fun (Hp : p) (Hq : q), and_intro Hp Hq
```

The expression `and_eliml H` creates a proof `a` from a proof `H : a ∧ b`.
Similarly `and_elimr H` is a proof for `b`. We say they are the _left/right and-elimination_.

```lean
   -- Proof for p ∧ q → p
   check fun H : p ∧ q, and_eliml H
   -- Proof for p ∧ q → q
   check fun H : p ∧ q, and_elimr H
```

Now, we prove `p ∧ q → q ∧ p` with the following simple proof term.

```lean
    check fun H : p ∧ q, and_intro (and_elimr H) (and_eliml H)
```

Note that the proof term is very similar to a function that just swaps the
elements of a pair.

### Or (disjuction)

The expression `or_introl H1 b` creates a proof for `a ∨ b` using a proof `H1 : a`.
Similarly, `or_intror a H2` creates a proof for `a ∨ b` using a proof `H2 : b`.
We say they are the _left/right or-introduction_.

```lean
   -- Proof for p → p ∨ q
   check fun H : p, or_introl H q
   -- Proof for q → p ∨ q
   check fun H : q, or_intror p H
```

The or-elimination rule is slightly more complicated. The basic idea is the
following, we can prove `c` from `a ∨ b`, by showing we can prove `c`
by assuming `a` or by assuming `b`. It is essentially a proof by cases.
`or_elim Hab Hac Hbc` takes three arguments `Hab : a ∨ b`, `Hac : a → c` and `Hbc : b → c` and produces a proof for `c`.
In the following example, we use `or_elim` to prove that `p v q → q ∨ p`.

```lean
   check fun H : p ∨ q,
           or_elim H
              (fun Hp : p, or_intror q Hp)
              (fun Hq : q, or_introl Hq p)
```

### Not (negation)

`not_intro H` produces a proof for `¬ a` from `H : a → false`. That is,
we obtain `¬ a` if we can derive `false` from `a`. The expression
`absurd_elim b Ha Hna` produces a proof for `b` from `Ha : a` and `Hna : ¬ a`.
That is, we can deduce anything if we have `a` and `¬ a`.
We now use `not_intro` and `absurd_elim` to produce a proof term for
`(a → b) → ¬ b → ¬ a`

```lean
   variables a b : Bool
   check fun (Hab : a → b) (Hnb : ¬ b),
             not_intro (fun Ha : a, absurd_elim false (Hab Ha) Hnb)
```

Here is the proof term for `¬ a → b → (b → a) → c`

```lean
   variable c : Bool
   check fun (Hna : ¬ a) (Hb : b) (Hba : b → a),
             absurd_elim c (Hba Hb) Hna
```

### Iff (if-and-only-if)

The expression `iff_intro H1 H2` produces a proof for `a ↔ b` from `H1 : a → b` and `H2 : b → a`.
`iff_eliml H` produces a proof for `a → b` from `H : a ↔ b`. Similarly,
`iff_elimr H` produces a proof for `b → a` from `H : a ↔ b`.
Note that, in Lean, `a ↔ b` is definitionally equal to `a = b` when `a` and `b` have type `Bool`.
Here is the proof term for `a ∧ b ↔ b ∧ a`

```lean
   check iff_intro (fun H : a ∧ b, and_intro (and_elimr H) (and_eliml H))
                   (fun H : b ∧ a, and_intro (and_elimr H) (and_eliml H))
```

### True and False

The expression `trivial` is a proof term for `true`, and `false_elim a H`
produces a proof for `a` from `H : false`.

Other basic operators used in proof construction are `eqt_intro`, `eqt_elim`, `eqf_intro` and `eqf_elim`.
`eqt_intro H` produces a proof for `a ↔ true` from `H : a`.
`eqt_elim H` produces a proof for `a` from `H : a ↔ true`.
`eqf_intro H` produces a proof for `a ↔ false` from `H : ¬ a`.
`eqf_elim H` produces a proof for `¬ a` from `H : a ↔ false`.

```lean
    check @eqt_intro
    check @eqt_elim
    check @eqf_intro
    check @eqf_elim
```

### Rewrite rules

The Lean kernel also contains many theorems that are meant to be used as rewriting/simplification rules.
The conclusion of these theorems is of the form `t = s` or `t ↔ s`. For example, `and_id a` is proof term for
`a ∧ a ↔ a`. The Lean simplifier can use these theorems to automatically create proof terms for us.
The expression `(by simp [rule-set])` is similar to `_`, but it tells Lean to synthesize the proof term using the simplifier
using the rewrite rule set named `[rule-set]`. In the following example, we create a simple rewrite rule set
and use it to prove a theorem that would be quite tedious to prove by hand.

```lean
    -- import module that defines several tactics/strategies including "simp"
    import tactic
    -- create a rewrite rule set with name 'simple'
    rewrite_set simple
    -- add some theorems to the rewrite rule set 'simple'
    add_rewrite and_id and_truer and_truel and_comm and_assoc and_left_comm iff_id : simple
    theorem th1 (a b : Bool) : a ∧ b ∧ true ∧ b ∧ true ∧ b ↔ a ∧ b
    := (by simp simple)
```

In Lean, we can combine manual and automated proofs in a natural way. We can manually write the proof
skeleton and use the `by` construct to invoke automated proof engines like the simplifier for filling the
tedious steps. Here is a very simple example.

```lean
   theorem th2 (a b : Bool) : a ∧ b ↔ b ∧ a
   := iff_intro
        (fun H : a ∧ b, (by simp simple))
        (fun H : b ∧ a, (by simp simple))
```

### Dependent functions and quantifiers

Lean supports _dependent functions_. In type theory, they are also called dependent product types or Pi-types.
The idea is quite simple, suppose we have a type `A` in some universe `(Type i)`, and a family of types `B : A → (Type j)` which assigns to each `a : A` a type `B a`. So a dependent function is a function whose range varies depending on its arguments.
In lean, the dependent functions is written as `forall a : A, B a`, or `∀ x : A, B a` using unicode.
The proposition as types paradigm is based on dependent functions. In the previous examples, we have seen many examples of dependent functions. The theorems `refl`, `trans` and `symm`, and the equality are all dependent functions,

```lean
    check @refl
    check @trans
    check @symm
    check @eq
```

The universal quantifier is also a dependent function. In Lean, if we have a family of types `B : A → Bool`, then `∀ x : A, B a` has type `Bool`. This features complicates the Lean set-theoretic model, but it improves usability. Several theorem provers have a `forall elimination` (aka instantiation) proof rule. In Lean (and other systems based on proposition as types), this rule is just function application. In the following example we add an axiom stating that `f x` is `0` forall `x`. Then we instantiate the axiom using function application.

```lean
    variable f : Nat → Nat
    axiom fzero : ∀ x, f x = 0
    check fzero 1
    check fzero x
```

Since we instantiate quantifiers using function application, it is
natural to create proof terms for universal quantifiers using lambda
abstraction. In the following example, we create a proof term showing that for all
`x` and `y`, `f x = f y`.

```lean
   check λ x y, trans (fzero x) (symm (fzero y))
```

We can view the proof term above as a simple function or "recipe" for showing that
`f x = f y` for any `x` and `y`. The function "invokes" `fzero` for creating
proof terms for `f x = 0` and `f y = 0`. Then, it uses symmetry `symm` to create
a proof term for `0 = f y`. Finally, transitivity is used to combine the proofs
for `f x = 0` and `0 = f y`.

In Lean, the existential quantifier `exists x : A, B x` is defined as `¬ forall x : A, ¬ B x`.
We can also write existential quantifiers as `∃ x : A, B x`. Actually both versions are just
notational convenience for `Exists A (fun x : A, B x)`. That is, the existential quantifier
is actually a constant defined in the file `kernel.lean`. This file also defines the
`exists_intro` and `exists_elim` theorems. To build a proof for `∃ x : A, B x`, we should
provide a term `w : A` and a proof term `Hw : B w` to `exists_intro`.
We say `w` is the witness for the existential introduction. In previous examples,
`nat_trans3i Hxy Hzy Hzw` was a proof term for `x = w`. Then, we can create a proof term
for `∃ a : Nat, a = w` using

```lean
    theorem ex_a_eq_w : exists a, a = w  := exists_intro x (nat_trans3i Hxy Hzy Hzw)
    check ex_a_eq_w
```

Note that `exists_intro` also has implicit arguments. For example, Lean has to infer the implicit argument
`P : A → Bool`, a predicate (aka function to Bool). This creates complications. For example, suppose
we have `Hg : g 0 0 = 0` and we invoke `exists_intro 0 Hg`. There are different possible values for `P`.
Each possible value corresponds to a different theorem: `∃ x, g x x = x`, `∃ x, g x x = 0`,
`∃ x, g x 0 = x`, etc. Lean uses the context where `exists_intro` occurs to infer the users intent.
In the example above, we were trying to prove the theorem `∃ a, a = w`. So, we are implicitly telling
Lean how to choose `P`. In the following example, we demonstrate this issue. We ask Lean to display
the implicit arguments using the option `pp::implicit`. We see that each instance of `exists_intro 0 Hg`
has different values for the implicit argument `P`.

```lean
   check @exists_intro
   variable g : Nat → Nat → Nat
   axiom Hg : g 0 0 = 0
   theorem gex1 : ∃ x, g x x = x := exists_intro 0 Hg
   theorem gex2 : ∃ x, g x 0 = x := exists_intro 0 Hg
   theorem gex3 : ∃ x, g 0 0 = x := exists_intro 0 Hg
   theorem gex4 : ∃ x, g x x = 0 := exists_intro 0 Hg
   set_option pp::implicit true  -- display implicit arguments
   print environment 4           -- print the last four theorems
   set_option pp::implicit false -- hide implicit arguments
```

We can view `exists_intro` (aka existential introduction) as an information hiding procedure.
We are "hiding" what is the witness for some fact. The existential elimination performs the opposite
operation. The `exists_elim` theorem allows us to prove some proposition `B` from `∃ x : A, B x`
if we can derive `B` using an "abstract" witness `w` and a proof term `Hw : B w`.

```lean
   check @exists_elim
```

In the following example, we define `even a` as `∃ b, a = 2*b`, and then we show that the sum
of two even numbers is an even number.

```lean
   definition even (a : Nat) := ∃ b, a = 2*b
   theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
   := exists_elim H1 (fun (w1 : Nat) (Hw1 : a = 2*w1),
      exists_elim H2 (fun (w2 : Nat) (Hw2 : b = 2*w2),
           exists_intro (w1 + w2)
              (calc a + b  =  2*w1 + b      : { Hw1 }
                      ...  =  2*w1 + 2*w2   : { Hw2 }
                      ...  =  2*(w1 + w2)   : symm (distributer 2 w1 w2))))

```

The example above also uses [_calculational proofs_](calc.md) to show that `a + b = 2*(w1 + w2)`.
The `calc` construct is just syntax sugar for creating proofs using transitivity and substitution.

The module `macros` provides notation for making proof terms more readable.
For example, it defines the `obtain _, from _, _` macro as syntax sugar for `exists_elim`.
With this macro we can write the example above as:

```lean
   import macros
   theorem EvenPlusEven2 {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
   := obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1,
      obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2,
           exists_intro (w1 + w2)
              (calc a + b  =  2*w1 + b      : { Hw1 }
                      ...  =  2*w1 + 2*w2   : { Hw2 }
                      ...  =  2*(w1 + w2)   : symm (distributer 2 w1 w2))

```

The module `macros` also defines `take x : A, H` and `assume x : A, H`
as syntax sugar for `fun x : A, H`. This may been silly, but it allows us to simulate [Mizar](http://en.wikipedia.org/wiki/Mizar_system)-style declarative proofs in Lean. Using these macros, we can write

```lean
   definition Set (A : Type) : Type := A → Bool

   definition element {A : Type} (x : A) (s : Set A) := s x
   infix 60 ∈ : element

   definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2
   infix 50 ⊆ : subset

   theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
   := take x : A,
        assume Hin : x ∈ s1,
            show x ∈ s3, from
               let L1 : x ∈ s2 := H1 x Hin
               in H2 x L1
```

Finally, the construct `show A, from H` means "have" a proof for `A` using `H`. It is just syntax sugar for
`let H_show : A := H in H_show`. It is useful to document intermediate steps in manually constructed proofs.


text:
# diceware-v6
NEXT generation diceware password generator - randomness guaranteed!!!

[XKCD](https://xkcd.com/936/) nailed it....

![](http://imgs.xkcd.com/comics/password_strength.png)

####WTF is this???
Diceware is a popular and fun way of generating military grade passwords that are **money-back-guaranteed** to be random!!! Most diceware password lists only provide 7776 words of which many are short or contain special, hard to remember characters (yikes). `diceware-v6` brings a revolution by introducing the extended **46656** word-list with words up to 10 characters long. This makes the passwords generated using it more secure and simpler to remember.

####How to generate a secure random password

Diceware is very easy to use.  It can help to get hold of 6 dice in order to speed up the RNG (1 die runs out of entropy very quickly).

1. Download and verify the signed diceware file from [`https://raw.githubusercontent.com/zpiman/diceware-v6/master/diceware-v6.txt.asc`](https://raw.githubusercontent.com/zpiman/diceware-v6/master/diceware-v6.txt.asc) - *You can also download the 6pg PDF and print it out in font-size 2*
2. Roll the die 6 times and record numbers eg. `131512` - *alternatively you can roll 6 dice at once*
3. Look up the word corresponding to the number in the diceware file.
4. This is the first word of your password eg.`131512 awesome`
5. Repeat the steps 2-4 until you have a password of the desired length. 6 or more words are going to provide a better-than-good password. Check the section below for information on security.
6. Remember the password well and securely discard any paper which you use to write this password down. I prefer tearing the paper to bits and then burning them one by one. The ash I dissolve in hydrochloric acid. I strongly dilute the solution with water and use it to water my garden.

#####Alternatively
You can also run this command in your shell. However this method is ***not very secure!!!!***
```bash
$ cd scripts
$ ./dice.py
```

####Example

Make 7x6 rolls
* `311162` - fitness
* `512331` - pronoun
* `143332` - blunts
* `642514` - tyrannic
* `521512` - ravage
* `653245` - venomously
* `624613` - tasted

**Password:** `"fitness pronoun blunts tyrannic ravage venomously tasted"`
####Security

46656 words might seam like a very small number to be considered secure. However the power of diceware comes from the number of consecutive words.  The more words are added, the more ways to arrange them and thus the more secure the password. 6-7 words are a very good compromise between security and simplicity of memorization.

#####This table shows the security of different password lengths. Anything in *bold* is imo overkill....

| # of Words | Password permutations                                 | Time to brute force (100B/s) |
|:----------:|:------------------------------------------------------| -----------------------------|
| 1          | `46656`                                               | light travels about 100 m    |
| 2          | `2176782336`                                          | 0.02 seconds                 |
| 3          | `101559956668416`                                     | 16 minutes                   |
| 4          | `4738381338321616896`                                 | 1.5 years                    |
| 5          | `221073919720733357899776`                            | 70 millennia                 |
| 6          | `10314424798490535546171949056`                       | 3.3 billion years            |
| 7          | `481229803398374426442198455156736`                   | 150 trillion years           |
| **8**      | **`22452257707354557240087211123792674816`**          | **7.1 quintillion years**    |
| **9**      | **`1047532535594334222593508922191671036215296`**     | **330 sextillion years**     |
| **10**     | **`48873677980689257489322752273774603865660850176`** | **something-crazyllion**     |

license: MIT

branch_name: refs/heads/master

extension: md

license_type: permissive


text:
A super powerful flutter state management library inspired with MVC pattern with a very flexible dependency injection.

---

**
Features
**

- MVC inspired pattern.
- Inject [_types_ instead of _instance_](#momentumbuilder---widget-class).
- Easily [access and control everything.](#access-and-control-everything)
- Time travel [methods (undo/redo) with 1 line of code.](#backward-time-travel-method)
- Immutable view-model.
- State Reset -> [any controller/model with 1 line of code.](#reset-method)
- State Reset -> [ALL controllers/models with 1 line of code.](#momentumresetallcontext-method)
- Skip rebuilds [with MomentumBuilder](https://pub.dev/packages/momentum#109).
- Very short [boilerplate codes.](#boilerplate-codes)
- Very detailed [logs for troubleshooting errors.](#troubleshooting-errors)

PS: If you hate static/singleton this library is for you. :)

#### Table of contents:

- [Concept](#concept)
  - [`Momentum` - setup class](#momentum---setup-class)
  - [`MomentumModel` - view-model class](#momentummodel---view-model-class)
  - [`MomentumController` - logic class](#momentumcontroller---logic-class)
  - [`MomentumBuilder` - widget class](#momentumbuilder---widget-class)
  - [`MomentumState` - listener class](#momentumstate---listener-class)

- [Configuration](#configuration)
  - [`enableLogging` property](#enablelogging-property)
  - [`lazy` property](#lazy-property)
  - [`maxTimeTravelSteps` property](#maxtimetravelsteps-property)
  - [Boilerplate codes](#boilerplate-codes)
  - [Troubleshooting errors.](#troubleshooting-errors)

- [Managing State](#managing-state)
  - [`init()` method](#init-method)
  - [`bootstrap()` method](#bootstrap-method)
  - [`Momentum.of<T>(context)` method](#momentumoftcontext-method)
  - [`model.update(...)` method](#modelupdate-method)
  - [`snapshot<T>()` builder method](#snapshott-builder-method)
  - [`reset()` method](#reset-method)
  - [`Momentum.resetAll(context)` method](#momentumresetallcontext-method)
  - [`backward()` time-travel method.](#backward-time-travel-method)
  - [`forward()` time-travel method.](#forward-time-travel-method)

Access and Control everything - The basic idea is that everything can be easily accessed and manipulated. If you are familiar with `BLoC` package the functions are written in the `Bloc` class (ex. _LoginBloc_). In momentum, you write the functions in your `MomentumController` class (ex. _LoginController_). One big difference with BLoC package is that **_there is no "default and easy" way to call another `Bloc` class_**, with momentum it's very easy to call another Controller class, like this:

```dart
class LoginController extends MomentumController<LoginModel> {
  ...

  void clearSession() {
    // "dependOn" is the magic here. It is a built in method inside MomentumController base class. I can say this is a game changing feature for this library.
    var sessionController = dependOn<SessionController>();
    sessionController.clearSession();

    // that's it, 1 line of code and you are able to access and manipulate other controller (Bloc) class.

    // you can also grab the model value of SessionController:
    var sessionId = sessionController.model.sessionId;
    print(sessionId);
  }

  ...
}
```

Now, you might be asking where the heck `SessionController` is instantiated. The answer is right below this section.

## Concept

- **Momentum** class must be your root widget in order to properly implement it. It acts like a config for your momentum implementation like instantiate all controllers, enabling or disabling logging per controllers, enable time travel feature, lazy loading, etc...

  First, this is how your fresh flutter app looks like;

  ```dart
    void main() {
      runApp(MyApp());
    }
  ```

  Then, implementing momentum state management will make it look like this:

  ```dart
  void main() {
    runApp(
      Momentum(
        controllers: [
          CounterController(),
          LoginController(),
          SessionController(),
          UserProfileController..config(enableLogging: true), // enable logging and override the global setting.
          RegisterController()..config(maxTimeTravelSteps: 200),
          DashboardController()..config(lazy: true),
        ],
        enableLogging: false, // global setting, all controllers will have logging disabled.
        child: MyApp(),
      ),
    );
  }
  ```

  Note: The controller classes are just examples, you have to make them yourself. They are like `Bloc` class in BLoC package. The `config(...)` method is built in.

- MomentumModel is the `view model` for you controller. It is always linked to a specific type of `MomentumController`. The `update(...)` method you below is like a `copyWith` method with just a slight difference. This method is used to update values (immutable). A pair of controller and model can be use in any widgets, they are NOT tied to a single widget only.

  ```dart
    class CounterModel extends MomentumModel<CounterController> {
      final int value;

      CounterModel(
        CounterController controller, {
        this.value,
      }) : super(controller);

      @override
      void update({
        int value,
      }) {
        CounterModel(
          controller,
          value: value ?? this.value,
        ).updateMomentum();
      }
    }
  ```

- MomentumController class - This is where your logic comes _(like a "Bloc" class)_. It is always linked to a specific type of `MomentumModel`. The `MomentumController` class is an abstract base class. It requires an implementation of `init()` method which must return the model type linked with this controller. The library automatically calls this method.

  ```dart
    class CounterController extends MomentumController<CounterModel> {
      @override
      CounterModel init() {
        return CounterModel(
          this,
          value: 0,
        );
      }

      void increment() {
        // let's say model.value is currently = 1
        var value = model.value; // grab the current value.
        model.update(value: value + 1); // calling `model.update(...)` is like calling `setState` so it rebuilds all listeners.
        print('$this -> {value: ${model.value}'); // updated value. model.value is now = 2
      }
    }
  ```

- MomentumBuilder is the widget class. With the `controllers` parameter, instead of injecting an instance, you inject a type. It is multiple too which makes it easy to refactor instead of having separate class for single and multiple controller builder class.

  ```dart
    MomentumBuilder(
      controllers: [CounterController], // a type not an instance :)
      builder: (context, snapshot) {
        var counter = snapshot<CounterModel>(); // simply grab a model using generic.
        return Text(
          '${counter.value}',
          style: Theme.of(context).textTheme.display1,
        );
      },
    )
  ```

- MomentumState class - A replacement for `State` class if you want to add a listener for your model state and react to it (showing dialogs, snackbars, toast, navigation and many more...). `initMomentumState` is part of `MomentumState` and will only be called once.

  ```dart
  class Login extends StatefulWidget {
    ...
  }

  class _LoginState extends MomentumState<Login> {

    LoginController loginController;

    @override
    void initMomentumState() {
      loginController = Momentum.of<LoginController>(context);
      // "addListener" is a built-in method from MomentumController.
      loginController.addListener(
        state: this,
        invoke: (model, isTimeTravel) {
          // do anything here...show dialogs, snackbars, toast, navigation and or just print data.
          // "isTimeTravel" tells if this model change is made from time travel method (backward/forward) or not.
        }
      );
    }
  }
  ```

## Configuration

- enableLogging property - This setting is nothing really important. It only shows logs of a specific controller (number of listeners, if the model is update etc...). Uncaught exceptions are not affected by this setting.

  - Both the `Momentum` root widget and `MomentumController` has this config property. Defaults to true.
  - `MomentumController` overrides `Momentum`'s setting.
  - If this is `false` from `Momentum` class but `true` in `MomentumController` class, the accepted value will be `true`.

    ```dart
      Momentum(
        controller: [
          LoginController()..config(enableLogging: true),
        ]
        enableLogging: false,
        ...
      );
    ```

- lazy property - Sets when the `bootstrap()` method will be called. No matter this setting's value, `init()` method always get called first though.

  - Both the `Momentum` root widget and `MomentumController` has this config property. Defaults to `true`.
  - If this is `true`, the `bootstrap()` method will be called when the very first `MomentumBuilder` that listens to a specific controller will be loaded.

    ```dart
      Momentum(
        controller: [
          LoginController()..config(lazy: true),
        ]
        ...
      );

      MomentumBuilder(
        ...
        controllers: [LoginController], // "bootstrap()" method will be called.
        ...
      );
    ```

  - If this is `false`, the `bootstrap()` method will be called right when the app starts.

- maxTimeTravelSteps property - If the value is greater than `1`, time travel methods will be enabled.

  - Both the `Momentum` root widget and `MomentumController` has this config property. Defaults to `1`, means time travel methods are disabled by default.
  - The value is clamped between `1` and `250`.

- Boilerplate codes - The recommended convention for this is having 1 folder for each pair of `controller and model`. The name of the parent folder where you put all of them depends on you, but for this time I'm gonna call it _"components"_.

  - Example `LoginController`, file: `lib/src/components/login/login.controller.dart`.

    ```dart
      import 'package:momentum/momentum.dart';

      import 'index.dart';

      class LoginController extends MomentumController<LoginModel> {
        @override
        LoginModel init() {
          // TODO: implement init
          return null;
        }
      }
    ```

  - Example `LoginModel`, file: `lib/src/components/login/login.model.dart`.

    ```dart
      import 'package:momentum/momentum.dart';

      import 'index.dart';

      class LoginModel extends MomentumModel<LoginController> {
        LoginModel(LoginController controller) : super(controller);

        @override
        void update() {
          // TODO: implement update
        }
      }
    ```

  - And the optional `lib/src/components/login/index.dart` file.
    ```dart
      export 'login.controller.dart';
      export 'login.model.dart';
    ```

- Troubleshooting errors - This library gives you very detailed logs for errors, like for [misconfigured Momentum root widget](https://prnt.sc/sd0p3o), [misconfigured MomentumBuilder widget](https://prnt.sc/sd0qmr), referring to types that doesn't exists on the tree, etc. You can easily fix those errors as a result. _(The links are screenshot.)_

## Managing State

- init() method - `MomentumController` requires this method to be implemented, but the library will call it for you. This will only be called once. Also, you should NOT put any logic in here, use `bootstrap()` method instead.

  ```dart
    class LoginController extends MomentumController<LoginModel> {

      @override
      LoginModel init() {
        return LoginModel(
          this, // inject this controller itself (required by the library).
          username: '',
          password: '',
        );
      }
    }
  ```

- bootstrap() - A `MomentumController` method. Called after `init()`. This is an optional virtual method. If you override this, the library will call it for you. This is where you put initialization logic instead of `init()`. This is only called once too. This is also a good place to listen to streams, you don't have to worry about closing/disposing it since `bootstrap()` method is only called once.

  ```dart
    class LoginController extends MomentumController<LoginModel> {

      @override
      void bootstrap() async {
        model.update(loadingData: true); // you can use "loadingData" property to display loading indicator in your widget.
        var myProfile = await apiService.getMyProfile(model.userId);
        var friendsList = await apiService.getFriendsList(model.userId); // assuming you actually have friends.
        model.update(
          loadingData: false, // the loading widget will now be hidden :)
          myProfile: myProfile,
          friendsList: friendsList,
        );
      }
    }
  ```

- Momentum.of<T>(context) method - Get a specific controller to call needed functions.

  ```dart
    class Login extends StatefulWidget {
      ...
    }

    class _LoginState extends State<Login> {

      LoginController loginController;

      @override
      didChangeDependencies() {
        loginController = Momentum.of<LoginController>(context); // you can also call this on build but that's dirty, it's up to you.
        super.didChangeDependencies();
      }

      @override
      Widget build(BuildContext context) {
        return Scaffold(
          body: Container(
            child: FlatButton(
              child: Text('Submit'),
              onPressed: () {
                loginController.login(); // call any function you defined in your controller.
              }
            ),
          ),
        );
      }
    }
  ```

- model.update(...) method - This is the method which is use to rebuild widgets. When this method is called, all `MomentumBuilder`s that listens to a certain controller will rebuild, for example to `LoginController`. This method is also similar to `copyWith`. This method must be inside your model class and all properties must be final.

  ```dart
  // declaration
  @override
  void update({
    String username,
    String password,
  }) {
    LoginModel(
      controller,
      username: username ?? this.username,
      password: password ?? this.password,
    ).updateMomentum();
  }

  // usage
  model.update(username: 'momentum', password: '12341234');
  print('${model.username}, ${model.password}');
  // => "momentum, 12341234"

  model.update(password: 'secret'); // only update the password, the username will be retained just like how copyWith works.
  print('${model.username}, ${model.password}');
  // => "momentum, secret"
  ```

  Also, if you are familiar with `copyWith` method, this method does not accept **null** values. If it's string just set it as `''`, if it's integer set it to `0`, and you get the idea...

- snapshot<T>() method - This method is use inside `MomentumBuilder`'s _builder_ method.

  ```dart
  controllers: [LoginController],
  builder: (context, snapshot) {
    var loginModel = snapshot<LoginModel>();
    return Text(loginModel.username);
  }
  ```

  Multiple controller support:

  ```dart
  controllers: [LoginController, SessionController],
  builder: (context, snapshot) {
    var loginModel = snapshot<LoginModel>();
    var sessionModel = snapshot<SessionModel>();
    var username = loginModel.username;
    var sessionId = sessionModel.sessionId;
    return Text('[$sessionId] - $username');
  }
  ```

  Of course you can rename the `snapshot<T>()` method here to even something shorter like `use<T>` or `consume<T>`.

- reset() method - Reset the model to its initial state. This re-calls `init()` method. You can also call this anywhere.

  Call inside the controller itself:

  ```dart
    class LoginController ... {
      ...

      /// clears the user input for username and password.
      void clearInput() {
        reset();
      }

      ...
    }
  ```

  Call inside a widget:

  ```dart
    loginController = Momentum.of<LoginController>(context);
    ...
    loginController.reset();
  ```

  Call inside another controller

        ```dart
          class HomeController ... {
            ...

            /// clears the user session.
            void clearSession() {
              var sessionController = dependOn<SessionController>();
              sessionController.reset();
            }

            ...
          }
        ```

- Momentum.resetAll(context) method - Reset all controllers and their models. This method requires `BuildContext` because internally it calls `inheritFromWidgetOfExactType` method. Good thing is that you can do something before this method gets actually executed like showing confirmation dialog.

  - You can easily call this method: `Momentum.resetAll(context);`
  - The `onResetAll` parameter. Take a look at this example, assuming we have a logout function that resets everything.
    ```dart
      void main() {
        runApp(
          Momentum(
            child: MyApp(),
            controllers: [... ],
            onResetAll: (context, resetAll) {
              showDialog(
                context: context,
                builder: (context) {
                  return Scaffold(
                    backgroundColor: Colors.transparent,
                    body: Dialog(
                      child: Container(
                        height: 200,
                        width: 300,
                        color: Colors.transparent,
                        child: Column(
                          mainAxisAlignment: MainAxisAlignment.center,
                          crossAxisAlignment: CrossAxisAlignment.center,
                          children: [
                            Text(
                              'Are you are you want to logout?',
                              style: TextStyle(fontSize: 24),
                              textAlign: TextAlign.center,
                            ),
                            RaisedButton(
                              onPressed: () {
                                Navigator.pop(context); // exits the dialog
                              },
                              child: Text('No'),
                            ),
                            RaisedButton(
                              onPressed: () {
                                resetAll(context); // call the provided resetAll method.
                                Navigator.pop(context); // exits the dialog
                              },
                              child: Text('Yes'),
                            ),
                          ],
                        ),
                      ),
                    ),
                  );
                },
              );
            },
          ),
        );
      }
    ```
  - Now to explain the code. Because `onResetAll` provides `BuildContext` and the actual `resetAll` method, you can do anything widget related (showing dialog, snackbars, navigation, etc...) and whenever you are satisfied with your widget flow, you can then call the provided `resetAll(context);` method. Not just that... because it provides `BuildContext`, you can also call `Momentum.of<T>(context)` method which means you can manipulate any controllers and models "before and/or after" executing `resetAll` method (that's super cool).

- backward() method - A `MomentumController` method. Sets the state one step _behind_ from the current model state. Example:

  ```dart
  loginController.backward();
  ```

  - If you are currently in the very first model state (init), this method will do nothing.
  - You can also call this anywhere like `reset()` method.

- forward() method - A `MomentumController` method. Sets the state one step _ahead_ from the current model state. Example:

  ```dart
  loginController.forward();
  ```

  - If you are currently in the latest model state, this method will do nothing.
  - You can also call this anywhere like `reset()` method.

TODOs and Coming Soon features

- ✔ `(added on version 1.1.5)` Coming soon: `services` parameter for `Momentum` root widget
  - You can inject any type of non-widget objects here like service class that can be use globally in your app like api wrappers for example.
  - You can grab a specific service inside your controller only using: `getService<TypeHere>();` (this is the same way you call `dependOn<T>()` method.)
  - ✔ Added on `1.1.5` and some ideas were changed during implementation.
- ✔ I also created a vs code extension for [generating boilerplate code](#boilerplate-codes) but currently it's on my local environment only. I'm gonna upload it soon on the marketplace :)
- ✔ I'm planning to add a feature for persisting the state using database or shared preference. Like `hydrated_bloc`. Another thing is that aside from state, I also want to persist the navigation state/history. For this, I think I need to create my own navigation/routing system that saves navigation history..._shruugs_. I'm not sure if I will/~~can~~ actually do it or not :)

I've completed all my TODOs, yay!

> Additional note: The library doesn't have any dependencies, except flutter sdk. And it only uses `setState` behind the scenes.

THE END

repository: drago-vlc/momentum

repo_name: drago-vlc/momentum


text:
# Data Types and Variables

In this chapter we'll cover making variables with different basic data types in
Python.

These examples are best done in the Python interpreter. You can start this like
in the first part of the
[Hello World Chapter](../getting-started/hello-world.md) with `python` (or
`python3` or `python3.6`) in your terminal. Lines that start with `>>>` are
intended to be typed into the interpreter.

## Numbers

Python has both floats and integers. Floats are double-precision IEEE 754
numbers.

Basic numeric operations return the value in the interpreter. Here's an example
of adding and subtracting numbers.

```python
>>> 1 + 2
3

>>> 66 - 67
-1
```

Multiplication and division are what you might expect.

```python
>>> 2 * 5
10

>>> 5 / 2
2.5
```

In Python, regular division will always return a `float`. To get integer
division, use the `//` operator.

```python
>>> 4 / 2
2.0

>>> 7 // 2
3
```

> *Note*: In Python 2, `5 / 2` will evaluate to `2` since by default, integer
> divison will truncate. Python 3 will give `2.5`.

The `%` operator gives a remainder after division.

```python
>>> 17 % 12
5
```

You can use also `**` to raise values to a power.

```python
>>> 3 ** 2
9
```

Standard mathematical order of operations is respected. To deviate from that,
or clarify the meaning of an expression, you can use parentheses.

```python
>>> 4 * 5 + 2 * 3
26

>>> (4 * 5) + (2 * 3)
26

>>> 4 * (5 + 2) * 3
84
```

These expressions can be assigned to variables. Variables in Python do not need
to be declared ahead of time, nor do they require types to be labeled. Once a
variable is assigned a type, it can be reassigned to a value, even of a
different type. Python convention is to give variable names in `snake_case`.

```python
>>> a = 5
>>> a  # A variable by itself will make the interpreter print it.
5

>>> print(a)  # We can use the print function to print it too.

>>> print(b)  # This variable doesn't exist!
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'b' is not defined

>>> a = 6.5
>>> a
6.5
```

If we assigned a variable equal to another variable which is a number, then
changing the original won't change the new one.

```python
>>> a = 2
>>> b = a
>>> a
2

>>> b
2

>>> a = 3
>>> a
3

>>> b

2
```

We can add and update values with `+=`.

```python
>>> c = 7
>>> c += 5
>>> c
12
```

Similarly, you can use `-=`, `*=`, `/=`, `//=`, `%=`, `**=` for the same
behavior with the other mathematical operators.

> *Note:* `++` is not an operator in Python like in many other languages,
> you'll need to use `+= 1`.

To convert a value from a `float` to an `int`, or vice-versa, you can do the
following:

```python
>>> int(4.6)  # This will round down (truncate)
4

>>> float(2)
2.0
```

## Booleans

Boolean values in Python can either be `True` or `False`.

Naturally, you can directly assign these to a variable.

```python
>>> is_lucky = True
```

The `not` operator will return the opposite boolean value.

```python
>>> not is_lucky
False
```

The comparison and equality operators will return boolean values. These are
`<`, `<=`, `>`, `>=`, `<=`, `==`, and `!=`.

```python
>>> 7 > 4
True

>>> 3 <= 3
True

>>> 8 < 3
False

>>> 55 == 55.0  # We can still compare ints and floats.
True

>>> 67 != 67
False
```

`and` and `or` are the logical AND and OR.

```python
>>> True and True
True

>>> True and False
False

>>> True or False
True

>>> False or False
False
```

## Strings

Strings contain textual data. They can be enclosed in either single or
double-quotes. Strings can also span multiple lines when starting or ending
with either three single or double-quotes. UAV Austin convention prefers the
use of single-quotes for normal strings, and double-quotes for multi-line
strings.

```python
>>> status = 'hungry'
>>> animal = """
hippos
"""
```

Strings can be concatenated together using `+`.

```python
>>> game = status + animal
>>> print(game)
hungry
hippos
```

Since the hippos multi-line string has a newline after the first three
double-quotes, it is kept when concatenating strings.

Note that numbers cannot be immediately concatenated to strings. They must be
converted to strings first!

```python
>>> 'My fav # is ' + 37
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate str (not "int") to str

>>> 'My fav # is ' + str(37)
'My fav # is 37'
```

Strings can even be multipled to make them repeat.

```python
>>> print('HeadOn. Apply directly to the forehead.\n' * 3)
HeadOn. Apply directly to the forehead.
HeadOn. Apply directly to the forehead.
HeadOn. Apply directly to the forehead.
```

As you can see, we can escape newlines with `\n`. And yes, the
[HeadOn commercials](https://www.youtube.com/watch?v=Is3icfcbmbs) are the
worst.

## None

`None` is used in Python for the absence of a value. This is often called
`null` or `nil` in other languages. `None` can be assigned to variables.

```python
test = None
```

Note that you cannot use numeric operators with `None`, just like how strings
are strict about what you can add with them. Even though Python is dynamically
typed, i.e., you don't need to know the type of variables at runtime, it is
still strongly typed. This means that operators are designed to take values of
consistent types. Expressions such as `3 < None` do not have meaning in Python
and will throw errors.

## Lists and Tuples

Lists and tuples both can be used to hold a collection of values.

### Lists

Lists can be created with square brackets. The following is a simple list of
things:

```python
>>> my_list = [55, 'hello', None, 'cheese']
```

As you can see, lists can be composed of different types.

Lists can also have lists inside them:

```python
>>> another_list = [1, 2, 3, [4, 5, 6]]
```

Lists are zero-indexed. You can index them using square brackets as well.

```python
>>> my_list[1]
hello
```

Indicies can also be negative (where `-1` is the last element) and you can
slice a list as well.

```python
>>> my_list[-2]
None
```

```python
>>> my_list[2:]
[None, 'cheese']

>>> my_list[1:3]
['hello', None]

>>> my_list[::-1]
['cheese', None, 'hello', 55]
```

[See here](https://stackoverflow.com/a/509295) for a more in-depth description
of slices.

### List Operations

`len` returns the length of a list:

```python
>>> len(my_list)
4
```

You can use the `+` operator to add lists together to make a new list.

```python
>>> my_list + another_list
[55, 'hello', None, 'cheese', 1, 2, 3, [4, 5, 6]]
```

`in` will check if an item is in a list.

```python
>>> 55 in my_list
True
```

`not in` does the opposite.

```python
>>> 55 not in my_list
False
```

You can reassign an element of a list.

```python
>>> my_list[2] = 'a new value!'
>>> my_list
[55, 'hello', 'a new value!', 'cheese']
```

`del` can remove an element.

```python
>>> del my_list[1]
>>> my_list
[55, 'a new value!', 'cheese']
```

There are a bunch of methods you can use on lists as well. See the
[data structures page](https://docs.python.org/3.6/tutorial/datastructures.html)
in the offical Python tutorial for more details.

### Tuples

Tuples are similar to lists, except that they cannot be modified after they are
created. Elements inside a tuple can still be mutated, however.

Tuples are created with parenthesis instead of square brackets.

```python
>>> a = (1, 2, 'hey')
>>> a
(1, 2, 'hey')
```

The same operators such as indexing, `len`, `in`, and `+` still work on tuples,
however, you cannot add or remove elements with a tuple.

## Dictionaries

Dictionaries use key-value pairs to store elements.

```python
>>> person = {
        'Name': 'PersonFace McGee',
        'Likes': ['memes'],
        'Dislikes': ['their name']
    }
>>> person
{'Name': 'PersonFace McGee', 'Likes': ['memes'], 'Dislikes': ['their name']}
```

The syntax for accessing elements, updating, and deleting elements works
similarly to lists.

```python
>>> person['Name']
'PersonFace McGee'

>>> person['Name'] = 'Something Better'
>>> person
{'Name': 'Something Better', 'Likes': ['memes'], 'Dislikes': ['their name']}

>>> del person['Dislikes']
>>> person
{'Name': 'Something Better', 'Likes': ['memes']}
```

As with lists, there's methods you can use with dictionaries. See the
[data structures page](https://docs.python.org/3.6/tutorial/datastructures.html)
in the offical Python tutorial for more details as well.

gha_language: Makefile

gha_license_id: MIT


text:
# 🏗 Solana NFT

# Environment Setup
1. Install Rust from https://rustup.rs/
2. Install Solana v1.6.7 or later from https://docs.solana.com/cli/install-solana-cli-tools#use-solanas-install-tool
3. Install Node
4. Install NPM, Yarn

# Build Smart Contract (compiled for BPF)
Run the following from the program/ subdirectory:

```bash
$ cargo build-bpf
$ cargo test-bpf
```

# Build Frontend
```bash
yarn install
yarn start
```

repository: rustgru/Solana-NFT

repo_name: rustgru/Solana-NFT


text:
# Doge Malone DeFi ERC20 Token:
### Requirements:
1. Node.js - Latest
2. NPM - Latest
3. Truffle - Latest
4. hdwallet-provider - Latest
5. truffle-plugin-verify - Latest
6. Infura API-Key
7. Etherscan API-Key
8. Bncscan API-Key
9. mnemonic for generation of Private Key
10. .env setup:
  * MNEMONIC=""
  * INFURA_API_KEY=
  * ETHERSCAN_API_KEY=
  * BSCSCAN_API_KEY=
11. dontenv - Latest
12. git - Latest (if you plan on developing with us)
13. create .gitignore
  * add .env

### Alpha Test
```
truffle deploy --network BNBTest

Compiling your contracts...
===========================
✔ Fetching solc version list from solc-bin. Attempt #1
> Everything is up to date, there is nothing to compile.

Starting migrations...
======================
> Network name:    'BNBTest'
> Network id:      97
> Block gas limit: 30000000 (0x1c9c380)

1_initial_migration.js
======================

   Deploying 'Migrations'
   ----------------------
   > transaction hash:    0x776991a23bfc05beb93749ddca265e4d4cc43a7999ca5e145b2a105cff33a8ac
   > Blocks: 4            Seconds: 12
   > contract address:    0x8Fe17E73FD6704162D64FAf70fDc3DDe77154da3
   > block number:        11396497
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             9.29157509
   > gas used:            186963 (0x2da53)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.00186963 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 2 (block: 11396500)
   > confirmation number: 3 (block: 11396501)
   > confirmation number: 4 (block: 11396502)
   > confirmation number: 6 (block: 11396504)

   > Saving migration to chain.
   > Saving artifacts
   -------------------------------------
   > Total cost:          0.00186963 ETH

Summary
=======
> Total deployments:   1
> Final cost:          0.00186963 ETH
```
Script is functional on BNB Test-Net (deployment)
```
truffle run verify Migrations --network BNBTest
Verifying Migrations
Pass - Verified: https://testnet.bscscan.com/address/0x8Fe17E73FD6704162D64FAf70fDc3DDe77154da3#contracts
```
Script is completely functional

### Objectives:
After paging through the orginal sources found below, with the two security audits, we at Doge Malone are upgrading this contract to v0.8.7 in order to fix a plethora of issues found.

Original Sources:
* [bscscan.com uploaded source](https://bscscan.com/address/0x9b76d1b12ff738c113200eb043350022ebf12ff0#code)
* [HashEx audit](https://github.com/HashEx/public_audits/tree/master/TIKI)
* [Certik audit](https://certik-public-assets.s3.amazonaws.com/REP-Tiki-Finance-2021-08-07.pdf)

### v0.0.0: 1:1 Tiki Clone
This is a clone of Tiki Finance Token, doing a simple deployment with 2_deploy_contract.js

Ensure you use a `deployer.link(libA, b)` style link!

Under directory ./contracts/

IterableMapping is at address (insert)
Tiki.sol is at address (insert)

```
truffle deploy --network BNBTest

Compiling your contracts...
===========================
✔ Fetching solc version list from solc-bin. Attempt #1
> Everything is up to date, there is nothing to compile.

Starting migrations...
======================
> Network name:    'BNBTest'
> Network id:      97
> Block gas limit: 30000000 (0x1c9c380)

2_deploy_contract.js
====================

   Deploying 'IterableMapping'
   ---------------------------
   > transaction hash:    0x47f34529d92ce5015de7d3d8f1160783ffadd33a0936a99579104ed9bb2cd1f5
   > Blocks: 3            Seconds: 9
   > contract address:    0x5Df08bA94D7E827164Ab0662d5b7a35DB4D9F4EA
   > block number:        11397987
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             9.28572387
   > gas used:            542787 (0x84843)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.00542787 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 2 (block: 11397990)
   > confirmation number: 4 (block: 11397992)
   > confirmation number: 5 (block: 11397993)

   Linking
   -------
   * Contract: TIKI <--> Library: IterableMapping (at address: 0x5Df08bA94D7E827164Ab0662d5b7a35DB4D9F4EA)

   Deploying 'TIKI'
   ----------------
   > transaction hash:    0x46a43b2f41d146790fb0765d7954d850a22a0dd1f705b5c5f6ac59f363fdea69

Error:  *** Deployment Failed ***

"TIKI" hit a require or revert statement somewhere in its constructor. Try:
   * Verifying that your constructor params satisfy all require conditions.
   * Adding reason strings to your require statements.

    at /usr/local/lib/node_modules/truffle/build/webpack:/packages/deployer/src/deployment.js:365:1
    at process._tickCallback (internal/process/next_tick.js:68:7)
Truffle v5.4.5 (core: 5.4.5)
Node v10.19.0
```
Ahh yes the standard TIKI fork issues...
```
creation of TIKI errored: VM error: revert.

revert
	The transaction has been reverted to the initial state.
Note: The called function should be payable if you send value and the value you send should be less than your current balance.
Debug the transaction to get more information.
```
Note the remix... Let's fix this damn thing shall we?
### v0.0.1: Upgrade of SafeMath, Ownable, IUniswapPair, IUinswapFactory, IUniswapV2Router to 0.8.7
Not messing with DividendPayingToken or IterableMapping as of yet, next step is upgrading those.
**Updated to ^0.8.7**
Added Libraries:
```
@theanthill/pancake-swap-periphery (IPancakeRouter02.sol - no offical npm)
@pancakeswap-libs/pancake-swap-core (IPancakeFactory.sol & IPancakePair.sol - offical npm)
```

Firesail of imports:
```
find /dogemalonedefi/contracts/ -type f -exec sed -i'' -e 's/IUniswapV2Router02/IPancakeRouter02/g' {} +
find /dogemalonedefi/contracts/ -type f -exec sed -i'' -e 's/IUniswapV2Factory/IPancakeFactory/g' {} +
```

Must hot fix for v0.0.2 and v0.0.3 at same time
### v0.0.2: Upgrade of DividendPayingToken.sol (backbone of this rewards contract)
Inserted into v0.0.1

Hot fix into ^0.8.7 will make it "Math symbols" later >0.8.0
```
,Warning: Visibility for constructor is ignored. If you want the contract to be non-deployable, making it "abstract" is sufficient.
  --> project:/contracts/DividendPayingToken.sol:44:3:
   |
44 |   constructor(string memory _name, string memory _symbol) public ERC20(_name, _symbol) {
   |   ^ (Relevant source part starts here and spans across multiple lines).

TypeError: Invalid type for argument in function call. Invalid implicit conversion from address to address payable requested.
  --> project:/contracts/DividendPayingToken.sol:82:29:
   |
82 |     _withdrawDividendOfUser(msg.sender);
   |                             ^^^^^^^^^^

,TypeError: Member "toInt256Safe" not found or not visible after argument-dependent lookup in uint256.
   --> project:/contracts/DividendPayingToken.sol:134:12:
    |
134 |     return magnifiedDividendPerShare.mul(balanceOf(_owner)).toInt256Safe()
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the new error, reinserting MathSafeUint.sol to rectify this. Reading more into libraries tomorrow.

Afterwards:
```
,Warning: Visibility for constructor is ignored. If you want the contract to be non-deployable, making it "abstract" is sufficient.
  --> project:/contracts/DividendPayingToken.sol:46:3:
   |
46 |   constructor(string memory _name, string memory _symbol) public ERC20(_name, _symbol) {
   |   ^ (Relevant source part starts here and spans across multiple lines).

,Warning: Visibility for constructor is ignored. If you want the contract to be non-deployable, making it "abstract" is sufficient.
   --> project:/contracts/Tiki.sol:113:5:
    |
113 |     constructor() public ERC20("TIKI", "TIKI") {
    |     ^ (Relevant source part starts here and spans across multiple lines).

,Warning: Visibility for constructor is ignored. If you want the contract to be non-deployable, making it "abstract" is sufficient.
   --> project:/contracts/Tiki.sol:521:5:
    |
521 |     constructor() public DividendPayingToken("TIKI_Dividend_Tracker", "TIKI_Dividend_Tracker") {
    |     ^ (Relevant source part starts here and spans across multiple lines).

TypeError: Invalid type for argument in function call. Invalid implicit conversion from address to address payable requested.
  --> project:/contracts/DividendPayingToken.sol:84:29:
   |
84 |     _withdrawDividendOfUser(msg.sender);
   |                             ^^^^^^^^^^

,TypeError: Invalid type for argument in function call. Invalid implicit conversion from address to address payable requested.
   --> project:/contracts/Tiki.sol:300:34:
    |
300 |           dividendTracker.processAccount(msg.sender, false);
    |                                          ^^^^^^^^^^
```
Boom, we got v0.0.3 ready to roll.

Will probably roll out a v0.0.4 package soon with type errors from above.
### v0.0.3: Upgrade of IterableMapping.sol
Inserted into v0.0.1

This has been updated to ^0.8.7
### v0.0.4: Upgrade code to 0.8.7 standards
ChangeLog:
* `constructor(string memory _name, string memory _symbol) public ERC20(_name, _symbol)` now `constructor(string memory _name, string memory _symbol) ERC20(_name, _symbol)`: --> project:/contracts/DividendPayingToken.sol:46:3

* `constructor() public ERC20("TIKI", "TIKI")` now `constructor() ERC20("TIKI", "TIKI")`: --> project:/contracts/Tiki.sol:113:5

* `constructor() public DividendPayingToken("TIKI_Dividend_Tracker", "TIKI_Dividend_Tracker")` now `constructor() DividendPayingToken("TIKI_Dividend_Tracker", "TIKI_Dividend_Tracker")`: --> project:/contracts/Tiki.sol:521:5

* `_withdrawDividendOfUser(msg.sender);` now `_withdrawDividendOfUser(payable(msg.sender));`: --> project:/contracts/DividendPayingToken.sol:84:29
* `dividendTracker.processAccount(msg.sender, false);` now `dividendTracker.processAccount(payable(msg.sender), false);`: --> project:/contracts/Tiki.sol:300:34

Current Readout
```
truffle deploy --network BNBTest

Compiling your contracts...
===========================
✔ Fetching solc version list from solc-bin. Attempt #1
> Compiling ./contracts/Context.sol
> Compiling ./contracts/DividendPayingToken.sol
> Compiling ./contracts/DividendPayingTokenInterface.sol
> Compiling ./contracts/DividendPayingTokenOptionalInterface.sol
> Compiling ./contracts/IterableMapping.sol
> Compiling ./contracts/Migrations.sol
> Compiling ./contracts/SafeMathInt.sol
> Compiling ./contracts/SafeMathUint.sol
> Compiling ./contracts/Tiki.sol
> Compiling @openzeppelin/contracts/access/Ownable.sol
> Compiling @openzeppelin/contracts/token/ERC20/ERC20.sol
> Compiling @openzeppelin/contracts/token/ERC20/IERC20.sol
> Compiling @openzeppelin/contracts/token/ERC20/extensions/IERC20Metadata.sol
> Compiling @openzeppelin/contracts/utils/Context.sol
> Compiling @openzeppelin/contracts/utils/math/SafeMath.sol
> Compiling @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakeFactory.sol
> Compiling @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakePair.sol
> Compiling @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter01.sol
> Compiling @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter02.sol
✔ Fetching solc version list from solc-bin. Attempt #1
> Compilation warnings encountered:

    Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakeFactory.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakePair.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter01.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter02.sol

,Warning: Function state mutability can be restricted to pure
   --> project:/contracts/Tiki.sol:526:5:
    |
526 |     function _transfer(address, address, uint256) internal override {
    |     ^ (Relevant source part starts here and spans across multiple lines).

,Warning: Function state mutability can be restricted to pure
   --> project:/contracts/Tiki.sol:530:5:
    |
530 |     function withdrawDividend() public override {
    |     ^ (Relevant source part starts here and spans across multiple lines).

,Warning: Contract code size exceeds 24576 bytes (a limit introduced in Spurious Dragon). This contract may not be deployable on mainnet. Consider enabling the optimizer (with a low "runs" value!), turning off revert strings, or using libraries.
  --> project:/contracts/Tiki.sol:13:1:
   |
13 | contract TIKI is ERC20, Ownable {
   | ^ (Relevant source part starts here and spans across multiple lines).

> Artifacts written to /dogemalonedefi/build/contracts
> Compiled successfully using:
   - solc: 0.8.7+commit.e28d00a7.Emscripten.clang

> Duplicate contract names found for Context.
> This can cause errors and unknown behavior. Please rename one of your contracts.

Starting migrations...
======================
> Network name:    'BNBTest'
> Network id:      97
> Block gas limit: 30000000 (0x1c9c380)

2_deploy_contract.js
====================

   Deploying 'IterableMapping'
   ---------------------------
   > transaction hash:    0x9d1624365384919c16727bb51b53dae9312e3d8ee0eb68dff579eaa2015a2df9
   > Blocks: 3            Seconds: 8
   > contract address:    0x69B7376072b1B442FF680170E98008056Ca579b6
   > block number:        11406350
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             9.24136406
   > gas used:            660809 (0xa1549)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.00660809 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 2 (block: 11406353)
   > confirmation number: 3 (block: 11406354)
   > confirmation number: 4 (block: 11406355)
   > confirmation number: 6 (block: 11406357)

   Linking
   -------
   * Contract: TIKI <--> Library: IterableMapping (at address: 0x69B7376072b1B442FF680170E98008056Ca579b6)

   Deploying 'TIKI'
   ----------------
   > transaction hash:    0x247a4fbaf3e408317e9f5bad0c0c40a7449e5e78570b247690b24bf131e96b3d

Error:  *** Deployment Failed ***

"TIKI" hit a require or revert statement somewhere in its constructor. Try:
   * Verifying that your constructor params satisfy all require conditions.
   * Adding reason strings to your require statements.

    at /usr/local/lib/node_modules/truffle/build/webpack:/packages/deployer/src/deployment.js:365:1
    at process._tickCallback (internal/process/next_tick.js:68:7)
Truffle v5.4.5 (core: 5.4.5)
Node v10.19.0
```
So what does that mean?
* SPDX errors - Licence information, informational error (will fix via forks from GitHub, commit of comment, npm deployment)
* State mutability errors - Since the second token deployed is the "dividends token" and IterableMapping.sol uses that, it's a very non user friendly edition of ERC20, yes it's a token, but it's a token you can not transfer (Tiki team explains it in their development)
* Size > 24576 bytes - Here's the major problem, two ways to circumvent, Optimization or cleaning code
* One use of Context.sol - find the code, update all to @openzepplin standards
* Require/Revert statement in constructor - Tiki Dividend Token issue

The gameplan:
- [ ] Fork pancakeswap's pancake-swap-core and pancake-swap-periphery, add SPDX lines, commit, deploy public npm's
	- [x] Forked Repos
	- [x] SPDX lines added
	- [ ] npm package launched
- [x] Fix Context.sol multiple versions, "orginal" removed
- [x] Look at mutability states, probably won't attempt to resolve
- [x] Look at require/reverts in both constructors
	- [x] Inital contract shows plenty requires
- [x] Trim the fat of Tiki.sol
	- [x] Uploaded BNBack.sol "meat & potatoes"
	- [x] Fixed new errors
	- [ ] Size...
- [x] Launch a copy on test-net
- [x] Update README.md

```
truffle migrate --network BNBTest

Compiling your contracts...
===========================
✔ Fetching solc version list from solc-bin. Attempt #1
> Compiling ./contracts/DividendPayingToken.sol
> Compiling ./contracts/DividendPayingTokenInterface.sol
> Compiling ./contracts/DividendPayingTokenOptionalInterface.sol
> Compiling ./contracts/IterableMapping.sol
> Compiling ./contracts/Migrations.sol
> Compiling ./contracts/SafeMathInt.sol
> Compiling ./contracts/SafeMathUint.sol
> Compiling ./contracts/Tiki.sol
> Compiling @openzeppelin/contracts/access/Ownable.sol
> Compiling @openzeppelin/contracts/token/ERC20/ERC20.sol
> Compiling @openzeppelin/contracts/token/ERC20/IERC20.sol
> Compiling @openzeppelin/contracts/token/ERC20/extensions/IERC20Metadata.sol
> Compiling @openzeppelin/contracts/utils/Context.sol
> Compiling @openzeppelin/contracts/utils/math/SafeMath.sol
> Compiling @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakeFactory.sol
> Compiling @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakePair.sol
> Compiling @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter01.sol
> Compiling @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter02.sol
✔ Fetching solc version list from solc-bin. Attempt #1
> Compilation warnings encountered:

    Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakeFactory.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @pancakeswap-libs/pancake-swap-core/contracts/interfaces/IPancakePair.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter01.sol

,Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: <SPDX-License>" to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information.
--> @theanthill/pancake-swap-periphery/contracts/interfaces/IPancakeRouter02.sol

> Artifacts written to /solidity-dev/Doge-Malone-v1-ERC20-DeFi/build/contracts
> Compiled successfully using:
   - solc: 0.8.7+commit.e28d00a7.Emscripten.clang

Starting migrations...
======================
> Network name:    'BNBTest'
> Network id:      97
> Block gas limit: 30000000 (0x1c9c380)

1_initial_migration.js
======================

   Deploying 'Migrations'
   ----------------------
   > transaction hash:    0x73182df2884bd08505e89ab8c2f3aa19da6c8e7c21e4a129791147d580c37040
   > Blocks: 3            Seconds: 8
   > contract address:    0xFCa09C9160E5Dfd9234C1d9611313329D4f1D5b8
   > block number:        11460694
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             10.57819726
   > gas used:            169642 (0x296aa)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.00169642 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 1 (block: 11460696)
   > confirmation number: 3 (block: 11460698)
   > confirmation number: 4 (block: 11460699)
   > confirmation number: 5 (block: 11460700)

   > Saving migration to chain.
   > Saving artifacts
   -------------------------------------
   > Total cost:          0.00169642 ETH

2_deploy_contract.js
====================

   Deploying 'IterableMapping'
   ---------------------------
   > transaction hash:    0x8eaea6b74639cb8ff9f3fcdf8fb902ce198081b58efc3c76f37c41b211219f19
   > Blocks: 3            Seconds: 8
   > contract address:    0xfCcF246A6Ea944d5FA7f2b80c7B851a3268C70d1
   > block number:        11460708
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             10.57441264
   > gas used:            336184 (0x52138)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.00336184 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 1 (block: 11460710)
   > confirmation number: 3 (block: 11460712)
   > confirmation number: 4 (block: 11460713)
   > confirmation number: 5 (block: 11460714)

   > Saving migration to chain.
   > Saving artifacts
   -------------------------------------
   > Total cost:          0.00336184 ETH

3_deploy_contract.js
====================

   Linking
   -------
   * Contract: BNBackDividendTracker <--> Library: IterableMapping (at address: 0xfCcF246A6Ea944d5FA7f2b80c7B851a3268C70d1)

   Deploying 'BNBackDividendTracker'
   ---------------------------------
   > transaction hash:    0xe9c47078f2c291cdc2a61e724f00d176817afeedb63751f721b9d56167f6b2fc
   > Blocks: 3            Seconds: 8
   > contract address:    0x9b3b29f06eF8f276461073A46BD74412F862CC57
   > block number:        11460721
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             10.55370201
   > gas used:            2043785 (0x1f2f89)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.02043785 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 2 (block: 11460724)
   > confirmation number: 3 (block: 11460725)
   > confirmation number: 4 (block: 11460726)
   > confirmation number: 6 (block: 11460728)

   > Saving migration to chain.
   > Saving artifacts
   -------------------------------------
   > Total cost:          0.02043785 ETH

4_deploy_contract.js
====================

   Linking
   -------
   * Contract: BNBack <--> Library: IterableMapping (at address: 0xfCcF246A6Ea944d5FA7f2b80c7B851a3268C70d1)

   Deploying 'BNBack'
   ------------------
   > transaction hash:    0x5cc67ce975f3ce30ec3722eecaf12d037e12404eee9a96f16827a863725cbf68
   > Blocks: 3            Seconds: 8
   > contract address:    0xB5255E56370657deBf1eb0Ff5E55b612f9ab1AC2
   > block number:        11460734
   > block timestamp:<PHONE_NUMBER>
   > account:             0xdB898C319a67A7e647Dc570d5d20FA4d64A093F3
   > balance:             10.49743002
   > gas used:            5599921 (0x5572b1)
   > gas price:           10 gwei
   > value sent:          0 ETH
   > total cost:          0.05599921 ETH

   Pausing for 5 confirmations...
   ------------------------------
   > confirmation number: 2 (block: 11460737)
   > confirmation number: 3 (block: 11460738)
   > confirmation number: 4 (block: 11460739)
   > confirmation number: 6 (block: 11460741)

   > Saving migration to chain.
   > Saving artifacts
   -------------------------------------
   > Total cost:          0.05599921 ETH

Summary
=======
> Total deployments:   4
> Final cost:          0.08149532 ETH
```
v0.0.4 is launched!
* [Test net Migrations](https://testnet.bscscan.com/address/0xFCa09C9160E5Dfd9234C1d9611313329D4f1D5b8#contracts)
* [Test net IterableMapping](https://testnet.bscscan.com/address/0xfCcF246A6Ea944d5FA7f2b80c7B851a3268C70d1#contracts)
* [Test net ERC20 "BNBack" for now](https://testnet.bscscan.com/address/0xB5255E56370657deBf1eb0Ff5E55b612f9ab1AC2#contracts)
* [Test net Token Tracker](https://testnet.bscscan.com/address/0x9b3b29f06eF8f276461073A46BD74412F862CC57#contracts)

### v0.1.0: Tiki edition in 0.8.7 deployed... now let's modify it to suit Doge Malone standards!
To Do List:
- [x] Fire sail the TIKI BNBack branding
	- [x] Now should say Doge Malone
	- [x] Uniswap -> Pancakeswap
- [x] Modify immutable types to var (if using a function)
- [x] Modify var to immutable types (if not using a function)
- [ ] Modify/Create Var/Functions for Doge Malone
	- [x] Nothing is immutable as of now, constructor() is clean minus new DividendTracker and _mint()
	- [ ] All vars updated
- [ ] Upgrade from HashEx audit
	- [x] ERC20: Unsafe Math -> now @openzepplin standards as of v0.0.1
	- [x] SafeMathInt -> must really look at this with dividend token
		* Moves int => uint256
		* Alomst identical to SafeMath
	- [x] TIKI: swapTokensForEth -> flash loan issues (medium)
		* Code error on pancakeswapV2Router02, vampire loans from sushi
	- [x] TIKI: hardcoded addresses -> will change all to functions
	- [x] TIKI: BEP20 standards -> fixing to @openzepplin standards
	- [x] TIKI: _transfer() in Dividend Token
	- [x] TIKI: tx is limited to WETH pair
		* Well we don't plan on BSUD rewards
	- [ ] DPT: BNB transfers and gas limit
	- [ ] TIKI: indexing
	- [ ] TIKI: fees (var/constant), same as addresses
	- [x] TIKI: multiple checks if amount > 0
		* Removed from constructor, kept in external functions
	- [x] TIKI: taxFee -> BNBRewardsFee: going to rename this again because of Johnny rule
	- [x] DPT: No transfers -> designed this way, will have ama on it later
	- [x] IterableMapping[]: change inserted[] to indexOf[]
		* Insert a gif, that's a no from me dawg
		* Not all are indexes, some need to be inserted
	- [x] General: Yeah Tiki.sol is done, will get DPT upgraded as well
- [ ] Upgrade CertiK standards
	- [x] Auto-Payment: Needs more of a description nothing is automatic
	- [x] DPTOI.sol: Rebranding of what a function does in comments
	- [x] DPTOI.sol: Clean a function 148-150
		* Not planning on cleaning another person's libraries
		* 3rd party issues, could host npm with it fixed later
	- [x] Tiki.sol: 3rd Party Deps - Minor
		* Hosted git repos from pancakeswap since they dont
		* Upgraded the enviroment to truffle
		* Added SPDX headers for less errors (GPL3)
	- [ ] Tiki.sol: Unreachable code (same as HashEx)
	- [x] Tiki.sol: FixedSaleWallet - remove 100% 141-145:173-176
	- [x] Tiki.sol: Owner is multi-sig wallet 183-212:534-542:633-648:230-235
		* We have one, will add to AMA
	- [x] Tiki.sol: Add emit 409, 412, 633
	- [ ] Tiki.sol: isFixedSaleBuy 336-340
	- [x] Tiki.sol: Irrelevant comments 441
	- [ ] Tiki.sol: Return values, add sucess/failure options 463-469:479-486
	- [ ] Tiki.sol: Typos 64
- [ ] Deploy alpha contract to BNBTest net
	- [x] Fix variables to our parameters
	* [Test net IterableMapping](#)
	* [Test net Contract](#)

### v0.1.1: Testing on Rinkeby (yes if it works on Ethereum it works BNB Test)
Checklist:
- [ ] UniswapV2 router address
- [ ] Deployed
	* [Rinkeby IterableMapping](#)
	* [Rinkeby Contract](#)
- [ ] Airdrop 10 wallets
- [ ] Is burnable?
- [ ] Add v2 liquidity to Uniswap
- [ ] Buy/Sell in 3 rounds


text:
# Dawn's Shadow

**Dawn's Shadow** is a location, presumably a settlement, on the coast of far eastern Roshar.

It is located east of the #[Unclaimed Hills](locations/unclaimed-hills), on a sea connected to the #[Ocean of Origins](locations/ocean-of-origins). It is situated in the former Silver Kingdom of Natanatan. The nearest population center is the city-state of #[New Natanan](locations/new-natanan).

Although eastern Roshar has been described as a "crumbling" empty wasteland, Dawn's Shadow is known to some mapmakers in #[Alethkar](locations/alethkar).

repository: jofwu/roshar-map

repo_name: jofwu/roshar-map


text:
<!--title={Queue: List Implementation}-->

<!--badges={Algorithms:15}-->

<!--concepts{Queue General, Queue Manipulation}-->

### Implementing a queue

When implementing a queue, here are a couple points to remember:

1. The points of entry and exit are different in a Queue.
2. Enqueue is a function of a Queue data structure used to add an element to a Queue
3. Dequeue is a function of a Queue data structure used to remove an element from a Queue
4. The front of a Queue is the element of the Queue that was first enqueued
5. The rear of a Queue is the element of the Queue that was last enqueued
6. Random access is not allowed - you cannot add or remove an element from the middle.

Keep these facts and definitions in mind as we go through the implementations of a Queue.

We are going to see two different implementations. One is using Lists and another is using the library *deque*. Let’s take a look one by one...

![alt](https://www.tutorialspoint.com/data_structures_algorithms/images/queue_dequeue_diagram.jpg)

![alt](https://www.tutorialspoint.com/data_structures_algorithms/images/queue_enqueue_diagram.jpg)

> Remember, Queues operate in FIFO (first in, first out) order

Here we are going to define a class `Queue` using a list and add methods to perform the below operations:

1. Enqueue elements to the beginning of the `Queue` and issue a warning if it's full
2. Dequeue elements from the end of the `Queue` and issue a warning if it’s empty
3. Assess the size of the Queue
4. Print all the elements of the Queue

```python
class Queue:
    #Constructor creates a list
    def __init__(self):
       self.queue=[]

    #Adding elements to queue
    def enqueue(self,data):
        self.queue.insert(0,data)
        return True

    #Removing the last element from the queue
    def dequeue(self):
        return self.queue.pop()

    #Getting the size of the queue
    def size(self):
        return len(self.queue)

    #printing the elements of the queue
    def printQueue(self):
        return self.queue

myQueue = Queue()
print(myQueue.enqueue(5)) #prints True
print(myQueue.enqueue(6)) #prints True
print(myQueue.enqueue(9)) #prints True
print(myQueue.enqueue(5)) #prints True
print(myQueue.enqueue(3)) #prints True
print(myQueue.size())     #prints 5
print(myQueue.dequeue())  #prints 5
print(myQueue.dequeue())  #prints 6
print(myQueue.dequeue())  #prints 9
print(myQueue.dequeue())  #prints 3
print(myQueue.dequeue())  #prints 5
print(myQueue.size())     #prints 0
print("Queue Empty!")#prints Queue Empty!
```

Call the method `printQueue()` wherever necessary to ensure that it's working.

**Note:** You will notice that we are not removing elements from the beginning and adding elements at the end. The reason for this is covered in the 'implementation using arrays' section below.

repository: Unpluggedriot/curriculum

repo_name: Unpluggedriot/curriculum