Instantly share code, notes, and snippets.

✍️
Visit my blog https://vitorsalmeida.com/

# vitor vit0rr

✍️
Visit my blog https://vitorsalmeida.com/
Created August 13, 2023 01:42
Proof in Coq that natural numbers are infinity
View a.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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'.
Created January 24, 2023 22:10 — forked from EduardoRFS/como_pensar.md
View como_pensar.md

# 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

Created December 30, 2022 18:43 — forked from sidneys/youtube_format_code_itag_list.md
YouTube video stream format codes itags

# 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 - - -
Created December 14, 2022 20:50 — forked from EduardoRFS/weak_self_types.md
View weak_self_types.md
```// 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;```
Created November 27, 2022 02:07
idk
View justOneDraft.res
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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)
Last active November 20, 2022 12:22
Como iniciar no Rust?
View start.md

A maneira mais comum para começar a estudar Rust é ler o livro oficial da linguagem. Irá ensinar sobre vários dos conceitos mais importantes sobre a linguagem.

A leitura pode ser acompanhada por:

Last active October 30, 2022 00:52
Church encoding of True, False and Or
View boolean-churchEncoding.ts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 type TRUE = (a: A) => (b: B) => A; type FALSE = (a: A) => (b: B) => B; type OR = (a: A) => (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;
Created October 17, 2022 03:28
Insertion sort example with TS
View insertionSort.ts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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];
Created October 11, 2022 13:08 — forked from Grubba27/fizzbuzz.ts