vitorsouzaalmeida

Theorem plus_1_n : forall n : nat, n + 1 = S n /\ S n > n.
Proof.
  intros n.
  split.
  - induction n as [| n' IHn'].
    + simpl. reflexivity.
    + simpl. rewrite <- IHn'. reflexivity.
  - induction n as [| n' IHn'].
    + simpl. apply le_n.
    + simpl. apply le_n_S. apply IHn'.

vitorsouzaalmeida

Code is clean if it can be understood easily – by everyone on the team. Clean code can be read and enhanced by a developer other than its original author. With understandability comes readability, changeability, extensibility and maintainability.

---

General rules

1. Follow standard conventions.
2. Keep it simple stupid. Simpler is always better. Reduce complexity as much as possible.
3. Boy scout rule. Leave the campground cleaner than you found it.
4. Always find root cause. Always look for the root cause of a problem.

Design rules

vitorsouzaalmeida

// ~/.config/borders/bordersrc

options=(
        style=round
        width=3.0
        hidpi=on
        active_color=0xffe2e2e3
        inactive_color=0xff414550
)

vitorsouzaalmeida

type id = string
type binop = Plus | Minus | Times 

type stm = CompoundStm of stm * stm
  | AssignStm of id * exp
  | PrintStm of exp list
  and exp = IdExp of id
  | NumExp of int
  | OpExp of exp * binop * exp
  | EseqExp of stm * exp