// 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;
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 Reverse<A> = | |
`${A}` extends `${infer AH}${infer AT}` | |
? `${Reverse<AT>}${AH}` : A | |
type Digs = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | |
type DigsNext<I = Digs, R = {}> = | |
I extends [infer Head, infer Next, ...infer Tail] |
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)
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.
- Follow standard conventions.
- Keep it simple stupid. Simpler is always better. Reduce complexity as much as possible.
- Boy scout rule. Leave the campground cleaner than you found it.
- Always find root cause. Always look for the root cause of a problem.