Standard escape codes are prefixed with Escape:
- Ctrl-Key:
^[ - Octal:
\033 - Unicode:
\u001b - Hexadecimal:
\x1B - Decimal:
27
This file contains hidden or 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
| def strict : Bool -> Type | |
| | true => Unit | |
| | false => Empty | |
| def f : (n:Nat) -> strict (n > 0) -> Nat := by | |
| intros n | |
| match n with | |
| | .zero => simp; exact fun i => by nomatch i | |
| | n@(.succ _) => simp; exact fun () => n |
blixt
/ gpt3_openai_monolog_qa.txt
Created
July 29, 2020 20:25
This file contains hidden or 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
| Q: Who are you? | |
| A: (I assume you're wondering about my name, but maybe also what I do.) I'm an AI that they call GPT-3. | |
| Q: What is human life expectancy in the United States? | |
| A: (The global life expectancy is 72.3 years so it should be around there.) Human life expectancy in the United States is 78 years. | |
| Q: Who was president of the United States in 1955? | |
| A: (Dwight D. Eisenhower served as president from 1953 to 1961.) Dwight D. Eisenhower was president of the United States in 1955. | |
| Q: What party did he belong to? |