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

vitorsouzaalmeida

// ~/.config/borders/bordersrc

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

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

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

Como Pensar

Ler e entender um pouco desse artigo. https://wiki.c2.com/?FeynmanAlgorithm

• Reconhecer como você pensa
• Descrever métodos que você usa para pensar
• Entender métodos diferentes de pensar
• Fazer perguntas sobre tudo(incluindo sobre perguntas)

Perguntas

vitorsouzaalmeida

YouTube video stream format codes

Comprehensive list of YouTube format code itags

itag Code	Container	Content	Resolution	Bitrate	Range	VR / 3D
5	flv	audio/video	240p	-	-	-
6	flv	audio/video	270p	-	-	-
17	3gp	audio/video	144p	-	-	-
18	mp4	audio/video	360p	-	-	-
22	mp4	audio/video	720p	-	-	-

vitorsouzaalmeida

// computing
C_bool = (A : Type) -> A -> A -> A;
(c_true : C_bool) = A => t => f => t;
(c_false : C_bool) = A => t => f => f;

// induction
I_bool b = (P : C_bool -> Type) -> P c_true -> P c_false -> P b;
i_true : I_bool c_true = P => p_t => p_f => p_t;
i_false : I_bool c_false = P => p_t => p_f => p_f;

vitorsouzaalmeida

let one = (f) => (x) => f(x) // (λf.λx.f x)
let two = (f) => (x) => f(f(x)) // (λf.λx.f (f x))

let _succ = (n) => (f) => (x) => f(n(f)(x)) // (λn.λf.λx.f (n f x))
let _add = (m) => (n) => (f) => (x) => m(f)(n(f)(x)) // (λm.λn.λf.λx.m f (n f x))
let _mult = (m) => (n) => (f) => (x) => m(n(f))(x) // (λm.λn.λf.λx.m (n f) x)
let _exp = (m) => (n) => (f) => (x) => n(m)(f)(x) // (λm.λn.λf.λx.n m f x)
let _pred = (n) => (f) => (x) => n((g) => (h) => h(g(f)))(u => x)(u => u) // (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u))
let _sub = (m) => (n) => n(_pred)(m) // (λm.λn.n pred m)

vitorsouzaalmeida

type TRUE = <A>(a: A) => <B>(b: B) => A;
type FALSE = <A>(a: A) => <B>(b: B) => B;
type OR = <A extends TRUE | FALSE>(a: A) => <B extends TRUE | FALSE>(b: B) => TRUE | FALSE;

// (λx.λy.x)
const TRUE: TRUE = a => b => a;
console.log(TRUE(1)(0));

// (λx.λy.y)
const FALSE: FALSE = a => b => b;

vitorsouzaalmeida

type Props = {
  length: number;
  arr: number[];
}

function insertionSort(arr: Props['arr']) {
  for (let i = 1; i < arr.length; i++) {
    let currentVal = arr[i];
    for (var j = i - 1; j >= 0 && arr[j] > currentVal; j--) {
      arr[j + 1] = arr[j];