-- This file:
--   http://anggtwu.net/SUBTITLES/2024-lean4-oficina-0.lua.html
--   http://anggtwu.net/SUBTITLES/2024-lean4-oficina-0.lua
--          (find-angg "SUBTITLES/2024-lean4-oficina-0.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun l () (interactive) (find-angg "SUBTITLES/2024-lean4-oficina-0.lua"))
-- (defun l () (interactive) (find-SUBS "2024-lean4-oficina-0.lua"))
-- (defun b () (interactive) (find-TH   "2024-lean4-oficina-0"))
-- (defun p () (interactive) (find-TH   "{ee-subs-pagestem}"))
-- (defun R () (interactive) (ee-recompile-SUBTITLES-0))
-- (defun r () (interactive) (ee-recompile-SUBTITLES-3))
-- (defun r () (interactive) (ee-recompile-SUBTITLES-1))
--  (define-key eev-mode-map (kbd "M-r") 'r)
--
-- Skel: (find-subs-links "2024lean4of0")
-- Old:  (find-editeevsubtitles-links-1 "2024lean4of0")
--       (find-efunction 'find-editeevsubtitles-links-1)
-- Yttr: (find-yttranscript-links       "2024lean4of0" "vBkxGIrv2Q0")
-- Info: (find-1stclassvideo-links      "2024lean4of0")
-- Play: (find-2024lean4of0video "0:00")
--
-- I use the code below to generate the subtitles in .vtt.
--

ee_dofile "~/LUA/Subtitles.lua" -- (find-angg "LUA/Subtitles.lua")

--[[
-- (find-angg "LUA/Subtitles.lua")

** Run the .lua and tell it to
** write the .vtt - by default in /tmp/
*
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2024-lean4-oficina-0.lua"
sts = Subtitles.fromsexps(subs_bigstr):addtime("37:20")
sts.lang = "pt-BR"
= sts
outfname = "$S/http/anggtwu.net/eev-videos/2024-lean4-oficina-0.vtt"
outfname =                           "/tmp/2024-lean4-oficina-0.vtt"
out = sts:vtt().."\n\n"
ee_writefile(outfname, out)
-- (find-fline                       "/tmp/2024-lean4-oficina-0.vtt")

** Test the .vtt
** (find-2024lean4of0video "0:00")

** Select /tmp/ or ee-eevvideosdir
** (find-eevvideosfile "")
** (find-eevvideosfile ""   "2024-lean4-oficina-0.mp4")
** (find-eevvideossh0 "cp -v 2024-lean4-oficina-0.mp4 /tmp/")
** (code-video "2024lean4of0video"                           "/tmp/2024-lean4-oficina-0.mp4")
** (code-video "2024lean4of0video" "$S/http/anggtwu.net/eev-videos/2024-lean4-oficina-0.mp4")
** (find-2024lean4of0video "0:00")

** Upload the 2024-lean4-oficina-0.vtt
** to http://anggtwu.net/eev-videos/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd /tmp/
scp    2024-lean4-oficina-0.vtt $LINP/eev-videos/
scp    2024-lean4-oficina-0.vtt $LINS/eev-videos/
Scp-np 2024-lean4-oficina-0.vtt $TWUP/eev-videos/
Scp-np 2024-lean4-oficina-0.vtt $TWUS/eev-videos/

** Upload the subtitles to youtube
** http://www.youtube.com/watch?v=vBkxGIrv2Q0

** Check that the "psne subtitles" thing works
** (find-1stclassvideo-links "2024lean4of0")

--]]

--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2024-lean4-oficina-0.lua"
for li in subs_bigstr:gmatch("([^\n]+)") do
  local time,text = li:match('^.-"(.-)".-"(.*)"%)$')
  text = text:gsub("\\(.)", "%1")
  if time then print("  "..time.."  "..text) end
end

--]]


subs_bigstr = [==[
% (find-2024lean4of0video "00:00" " ")
% (find-2024lean4of0video "00:02" "Oi, gente! O meu nome é Eduardo Ochs, e eu tou")
% (find-2024lean4of0video "00:05" "pretendendo dar uma oficina de Lean4")
% (find-2024lean4of0video "00:08" "daqui um tempo... e esse vídeo é para")
% (find-2024lean4of0video "00:10" "explicar algumas coisas que seriam")
% (find-2024lean4of0video "00:11" "difíceis de explicar só por uma página")
% (find-2024lean4of0video "00:14" "na internet.")

% (find-2024lean4of0video "00:15" "Os dados da oficina vão estar todos")
% (find-2024lean4of0video "00:17" "aqui nessa URL, e essa daqui é minha")
% (find-2024lean4of0video "00:20" "página sobre Lean4.")

% (find-2024lean4of0video "00:22" "Primeiro: o que que é o Lean4?")
% (find-2024lean4of0video "00:24" "O Lean4 é parecido com Haskell, mas")
% (find-2024lean4of0video "00:27" "ele é bem mais fácil de instalar, e tem")
% (find-2024lean4of0video "00:30" "uma interface muito bacana que eu vou")
% (find-2024lean4of0video "00:32" "mostrar daqui a pouco. Ele pode ser usado")
% (find-2024lean4of0video "00:34" "como proof assistant - muita gente pensa")
% (find-2024lean4of0video "00:38" "nele como proof assistant, só que eu ainda")
% (find-2024lean4of0video "00:40" "não sei usar ele como proof assistant...")
% (find-2024lean4of0video "00:42" "eu comecei a aprender ele porque eu queria")
% (find-2024lean4of0video "00:46" "usar ele como proof assistant pra umas")
% (find-2024lean4of0video "00:47" "coisas super complicadas, e...")
% (find-2024lean4of0video "00:50" "ainda não sei o suficiente para isso...")

% (find-2024lean4of0video "00:52" "mas tou adorando ele como uma linguagem")
% (find-2024lean4of0video "00:54" "parecida com Haskell, e mais legal, com uma")
% (find-2024lean4of0video "00:58" "interface bacana, e tal...")

% (find-2024lean4of0video "01:00" "e o mais importante é que ele é muito")
% (find-2024lean4of0video "01:02" "extensível - no sentido de que é fácil")
% (find-2024lean4of0video "01:04" "você definir sintaxes novas nele... definir")
% (find-2024lean4of0video "01:08" "mini-linguagens, DSLs, todas essas coisas")
% (find-2024lean4of0video "01:11" "assim... se vocês quiserem explicações pra")
% (find-2024lean4of0video "01:13" "isso tem nesse manual daqui, já vou")
% (find-2024lean4of0video "01:15" "explicar qual é...")

% (find-2024lean4of0video "01:17" "então, um dos manuais principais do Lean4")
% (find-2024lean4of0video "01:19" "é o \"Metaprogramming in Lean4\",")
% (find-2024lean4of0video "01:22" "e aí um dos capítulos")
% (find-2024lean4of0video "01:25" "explica essa história de definir as")
% (find-2024lean4of0video "01:29" "sintaxes novas - nessa seção daqui.")

% (find-2024lean4of0video "01:36" "Voltando...")
% (find-2024lean4of0video "01:42" "Primeiro: quem é o público alvo dessa")
% (find-2024lean4of0video "01:45" "oficina?")
% (find-2024lean4of0video "01:48" "Vai ser uma oficina muito básica, e")
% (find-2024lean4of0video "01:52" "a ideia é que ela vai ser direcionada")
% (find-2024lean4of0video "01:54" "pra pessoas que tentaram aprender Haskell")
% (find-2024lean4of0video "01:57" "mas que empacaram mais ou menos nos mesmos")
% (find-2024lean4of0video "01:59" "lugares que eu.")

% (find-2024lean4of0video "02:00" "A partir de um determinado ponto os")
% (find-2024lean4of0video "02:02" "livros começam a mostrar umas coisas")
% (find-2024lean4of0video "02:04" "super complicadas e meio que exigir que")
% (find-2024lean4of0video "02:06" "a gente entenda todos os detalhes delas")
% (find-2024lean4of0video "02:08" "de cabeça... eles não dão nenhuma")
% (find-2024lean4of0video "02:10" "informação sobre como a gente poderia")
% (find-2024lean4of0video "02:12" "fazer as \"contas\" no papel pra conseguir")
% (find-2024lean4of0video "02:16" "entender os detalhes daquilo.")

% (find-2024lean4of0video "02:17" "Então - aqui tem um exemplo. Um")
% (find-2024lean4of0video "02:21" "amigo meu que tá trabalhando na Holanda...")
% (find-2024lean4of0video "02:25" "uma das tarefas dele como pós-doc é")
% (find-2024lean4of0video "02:29" "orientar os alunos que estão fazendo")
% (find-2024lean4of0video "02:32" "curso de Haskell lá... e eles usam o livro")
% (find-2024lean4of0video "02:36" "do Hutton, então eu tentei aprender a  usar")
% (find-2024lean4of0video "02:38" "livro do Hutton também... a capa dele é essa,")
% (find-2024lean4of0video "02:42" "aqui tá o índice do livro...")
% (find-2024lean4of0video "02:46" "e o capítulo 12 do livro é o capítulo")
% (find-2024lean4of0video "02:50" "onde ele começa a explicar mônadas.")

% (find-2024lean4of0video "02:53" "E aí ele...")
% (find-2024lean4of0video "02:56" "define umas coisas que eu só fui entender agora...")
% (find-2024lean4of0video "03:01" "eu já tentei decifrar esse capítulo várias")
% (find-2024lean4of0video "03:02" "vezes nos últimos três ou quatro anos e só")
% (find-2024lean4of0video "03:05" "comecei a entender agora...")

% (find-2024lean4of0video "03:07" "então, ele tem essas figurinhas aqui para")
% (find-2024lean4of0video "03:09" "explicar o que que é uma \"state monad\".")
% (find-2024lean4of0video "03:12" "E aí ele define")
% (find-2024lean4of0video "03:14" "essa coisa daqui, ó...")
% (find-2024lean4of0video "03:20" "ele diz que a gente vai definir um tipo")
% (find-2024lean4of0video "03:22" "novo desse jeito daqui...")
% (find-2024lean4of0video "03:23" "e depois uma função \"app\", que usa esse tipo...")
% (find-2024lean4of0video "03:27" "depois uma função \"fmap\", que é uma instância")
% (find-2024lean4of0video "03:31" "do funtor ST, whatever that means...")
% (find-2024lean4of0video "03:34" "e aí ele põe essa figurinha daqui.")

% (find-2024lean4of0video "03:37" "Até hoje de tarde eu não fazia a menor")
% (find-2024lean4of0video "03:39" "ideia de se essa figura era uma coisa")
% (find-2024lean4of0video "03:40" "precisa ou não.")

% (find-2024lean4of0video "03:42" "Se fosse certamente estavam faltando")
% (find-2024lean4of0video "03:44" "muitos detalhes aqui, e")
% (find-2024lean4of0video "03:46" "eu ainda não tinha certeza de como")
% (find-2024lean4of0video "03:49" "completar esses detalhes.")

% (find-2024lean4of0video "03:51" "Então... deixa eu mostrar uma")
% (find-2024lean4of0video "03:53" "figura aqui.")

% (find-2024lean4of0video "03:56" "Essa primeira definição... essas duas")
% (find-2024lean4of0video "04:00" "definições daqui, essa e essa, estão nesse")
% (find-2024lean4of0video "04:04" "primeiro diagrama.")

% (find-2024lean4of0video "04:06" "Então, no livro do Hutton")
% (find-2024lean4of0video "04:07" "elas aparecem como essas três linhas")
% (find-2024lean4of0video "04:09" "daqui - essa definição de um newtype,")
% (find-2024lean4of0video "04:12" "depois o tipo da da função \"app\", depois a")
% (find-2024lean4of0video "04:14" "definição da \"app\" em si...")

% (find-2024lean4of0video "04:16" "e aí esse tipo de figura daqui")
% (find-2024lean4of0video "04:17" "me ajudou muito a decifrar essas coisas.")

% (find-2024lean4of0video "04:20" "Eu pego essa expressão daqui de baixo,")
% (find-2024lean4of0video "04:22" "e embaixo de cada subexpressão dela")
% (find-2024lean4of0video "04:24" "eu escrevo qual é o tipo dela.")

% (find-2024lean4of0video "04:27" "O ideal seria fazer uma animação")
% (find-2024lean4of0video "04:30" "dizendo quais são os tipos que eu")
% (find-2024lean4of0video "04:31" "descubro primeiro e como é que a")
% (find-2024lean4of0video "04:34" "inferência de tipos funciona, e como é")
% (find-2024lean4of0video "04:36" "que a gente vai descobrindo tudo aos")
% (find-2024lean4of0video "04:38" "poucos... mas nesse caso aqui eu ainda não")
% (find-2024lean4of0video "04:40" "fiz a animação.")

% (find-2024lean4of0video "04:42" "Então, a grande dificuldade para mim")
% (find-2024lean4of0video "04:44" "foi entender o que é essa operação S daqui")
% (find-2024lean4of0video "04:46" "e esse underbrace daqui...")

% (find-2024lean4of0video "04:51" "e o legal é que quando")
% (find-2024lean4of0video "04:53" "eu faço esse tipo de diagrama eu consigo")
% (find-2024lean4of0video "04:55" "apontar pra um underbrace e")
% (find-2024lean4of0video "04:57" "dizer: é esse o underbrace que eu")
% (find-2024lean4of0video "05:00" "ainda não tenho certeza... e depois de")
% (find-2024lean4of0video "05:02" "horas eu descobri que se eu")
% (find-2024lean4of0video "05:05" "escrevesse esse underbrace desse jeito")
% (find-2024lean4of0video "05:07" "daqui... desculpa, esse underbrace daqui...")
% (find-2024lean4of0video "05:12" "usando essa definição de newtype aqui, que diz")
% (find-2024lean4of0video "05:14" "que \"ST a\" é sempre equivalente a")
% (find-2024lean4of0video "05:16" "S (State→(a,State)),")
% (find-2024lean4of0video "05:18" "aí tudo ficava claro... aí as")
% (find-2024lean4of0video "05:22" "regras não ficavam mais tão")
% (find-2024lean4of0video "05:25" "misteriosas.")

% (find-2024lean4of0video "05:27" "Então, voltando.")
% (find-2024lean4of0video "05:30" "Até pouquíssimo tempo atrás eu não sabia")
% (find-2024lean4of0video "05:32" "decifrar")
% (find-2024lean4of0video "05:34" "trechos difíceis do Hutton - eu não")
% (find-2024lean4of0video "05:38" "sabia que ferramentas usar para")
% (find-2024lean4of0video "05:40" "completar os detalhes deles... e esse tipo")
% (find-2024lean4of0video "05:42" "de diagrama tem me ajudado muito.")

% (find-2024lean4of0video "05:45" "Agora vem o diagrama... opa, peraí...")
% (find-2024lean4of0video "05:49" "ah deixa eu mostrar o diagrama da página")
% (find-2024lean4of0video "05:52" "seguinte... aqui.")
% (find-2024lean4of0video "05:55" "Lembra que agora há pouco eu mostrei")
% (find-2024lean4of0video "05:57" "essa figurinha no livro do Hutton")
% (find-2024lean4of0video "06:00" "e disse que até pouco tempo atrás eu não")
% (find-2024lean4of0video "06:01" "fazia ideia de se essa figura era só uma...")
% (find-2024lean4of0video "06:06" "se ela era informal ou não...")
% (find-2024lean4of0video "06:08" "então, nessa página o o Hutton introduz")
% (find-2024lean4of0video "06:13" "algumas linhas a mais, aqui...")

% (find-2024lean4of0video "06:15" "ele diz que a gente vai definir o fmap desse")
% (find-2024lean4of0video "06:17" "jeito daqui, e aí ele mostra essa figura como")
% (find-2024lean4of0video "06:20" "se fosse óbvia... e para mim ela não é!")
% (find-2024lean4of0video "06:23" "Eu preciso fazer todas essas type")
% (find-2024lean4of0video "06:25" "inferences daqui para descobrir qual é o")
% (find-2024lean4of0video "06:27" "tipo")
% (find-2024lean4of0video "06:28" "da g da st, da s, da x, da s', etc, e")
% (find-2024lean4of0video "06:33" "das outras expressões que são compostas")
% (find-2024lean4of0video "06:35" "a partir delas... e aí quando eu descubro")
% (find-2024lean4of0video "06:38" "todos esses tipos daqui eu consigo")
% (find-2024lean4of0video "06:39" "transformar esse diagrama daqui num")
% (find-2024lean4of0video "06:41" "diagrama que tem não só esses símbolos")
% (find-2024lean4of0video "06:44" "que são nomes de termos, como esses tipos")
% (find-2024lean4of0video "06:48" "daqui...")
% (find-2024lean4of0video "06:50" "então esse s daqui é de tipo State")
% (find-2024lean4of0video "06:52" "essa coisa daqui é de tipo ST a, etc...")
% (find-2024lean4of0video "06:56" "e aí tudo fez sentido para mim.")

% (find-2024lean4of0video "07:00" "Então, voltando... agora eu preciso contar uma")
% (find-2024lean4of0video "07:02" "historinha, tá... eu vou contar ela de um")
% (find-2024lean4of0video "07:04" "jeito bem resumido e eu vou botar o link")
% (find-2024lean4of0video "07:06" "do lugar onde vocês podem ler o texto dela.")

% (find-2024lean4of0video "07:09" "Há um tempo atrás eu fiz dois")
% (find-2024lean4of0video "07:11" "vídeos sobre didática... um deles ficou")
% (find-2024lean4of0video "07:14" "muito bom e outro tem só alguns trechos bons.")
% (find-2024lean4of0video "07:16" "Esse vídeo é o que tem alguns trechos bons.")

% (find-2024lean4of0video "07:18" "E ele tem essa historinha que eu")
% (find-2024lean4of0video "07:22" "acho bem importante. É o seguinte... eu")
% (find-2024lean4of0video "07:25" "não vou ler ela toda agora, mas é")
% (find-2024lean4of0video "07:28" "uma história sobre alguém... um")
% (find-2024lean4of0video "07:30" "professor que ensina uma coisa super")
% (find-2024lean4of0video "07:31" "difícil, um aluno não entende e ele diz:")
% (find-2024lean4of0video "07:34" "\"mas isso é óbvio!\" Aí o aluno diz:")
% (find-2024lean4of0video "07:38" "\"não é óbvio não!\"... mas o aluno vai")
% (find-2024lean4of0video "07:40" "pra casa pensar, ele pensa, pensa, pensa muito,")
% (find-2024lean4of0video "07:42" "depois no dia seguinte ele volta e ele")
% (find-2024lean4of0video "07:46" "virou uma pessoa para quem aquilo é")
% (find-2024lean4of0video "07:47" "óbvio. Ele não sabe explicar pra as")
% (find-2024lean4of0video "07:49" "outras pessoas quais são os detalhes")
% (find-2024lean4of0video "07:51" "daquilo, ele só sabe dizer pras pessoas")
% (find-2024lean4of0video "07:54" "\"ah, isso é óbvio!\"... mas ele virou a")
% (find-2024lean4of0video "07:57" "pessoa para quem isso é óbvio.")

% (find-2024lean4of0video "08:00" "Eu não gosto dessa ideia de aprender coisas")
% (find-2024lean4of0video "08:02" "complicadas e virar uma pessoa que só")
% (find-2024lean4of0video "08:04" "sabe dizer \"ah, isso é óbvio!\", e e eu tou há")
% (find-2024lean4of0video "08:07" "vários anos trabalhando em alternativas")
% (find-2024lean4of0video "08:09" "pra isso. Essa alternativas são descobrir")
% (find-2024lean4of0video "08:12" "os diagramas que faltam e encontrar um")
% (find-2024lean4of0video "08:16" "jeito mais ou menos mecânico e formal de")
% (find-2024lean4of0video "08:19" "produzir esses diagramas que faltam.")

% (find-2024lean4of0video "08:21" "Então, essa oficina de Lean")
% (find-2024lean4of0video "08:24" "vai ser principalmente sobre um modo de")
% (find-2024lean4of0video "08:29" "produzir esses diagramas que faltam e de")
% (find-2024lean4of0video "08:31" "apresentar as coisas que os livros sobre Lean")
% (find-2024lean4of0video "08:33" "apresentam de um jeito muito difícil")
% (find-2024lean4of0video "08:36" "com esses diagramas.")

% (find-2024lean4of0video "08:38" "Então vou mostrar os pontos em que eu")
% (find-2024lean4of0video "08:40" "empacava... e que ficaram")
% (find-2024lean4of0video "08:42" "muito mais simples depois que eu aprendi")
% (find-2024lean4of0video "08:43" "a fazer diagramas. Então: não tenho")
% (find-2024lean4of0video "08:45" "certeza se esses diagramas vão funcionar")
% (find-2024lean4of0video "08:48" "pra outras pessoas - é isso que eu quero")
% (find-2024lean4of0video "08:50" "testar - mas são os diagramas que")
% (find-2024lean4of0video "08:52" "funcionaram para mim.")

% (find-2024lean4of0video "08:54" "E aí eu quero")
% (find-2024lean4of0video "08:56" "descobrir quais são as dificuldades dos")
% (find-2024lean4of0video "08:57" "outros, se isso faz sentido, se elas têm")
% (find-2024lean4of0video "09:00" "os tipos delas de diagramas e coisas")
% (find-2024lean4of0video "09:03" "do gênero...")

% (find-2024lean4of0video "09:04" "Então, tem um monte de técnicas")
% (find-2024lean4of0video "09:06" "didáticas por trás disso daqui...")
% (find-2024lean4of0video "09:09" "e eu também vou mostrar como eu")
% (find-2024lean4of0video "09:11" "transformei os exemplos dos livro de Lean")
% (find-2024lean4of0video "09:14" "em exemplos que são mais fáceis de testar")
% (find-2024lean4of0video "09:16" "passo a passo.")

% (find-2024lean4of0video "09:18" "E aí aqui tem tem um")
% (find-2024lean4of0video "09:20" "caso muito mais simples de")
% (find-2024lean4of0video "09:23" "de situação em que eu fiz algo parecido")
% (find-2024lean4of0video "09:26" "com essa técnica...")
% (find-2024lean4of0video "09:29" "eu peguei coisas que eram explicadas de")
% (find-2024lean4of0video "09:31" "um jeito complicado, com exemplos grandes...")
% (find-2024lean4of0video "09:33" "e desmontei os exemplos em exemplos")
% (find-2024lean4of0video "09:35" "muito simples. Então, por exemplo se a")
% (find-2024lean4of0video "09:37" "gente quiser aprender o que que é essa")
% (find-2024lean4of0video "09:38" "expressão aqui em Lisp eu posso")
% (find-2024lean4of0video "09:41" "desmontar ela em várias expressões")
% (find-2024lean4of0video "09:42" "pequenininhas, e aí eu posso executar")
% (find-2024lean4of0video "09:45" "cada uma dessas expressões - quando eu")
% (find-2024lean4of0video "09:47" "executo ela o resultado aparece aqui")
% (find-2024lean4of0video "09:49" "embaixo... e aí com isso eu tenho todas as")
% (find-2024lean4of0video "09:51" "expressões visíveis de uma vez, e eu")
% (find-2024lean4of0video "09:54" "consigo comparar duas expressões, ver")
% (find-2024lean4of0video "09:56" "onde é que tão as dificuldades ver onde")
% (find-2024lean4of0video "09:58" "aparece algum conceito novo, e coisas assim...")

% (find-2024lean4of0video "10:02" "e eu vou mostrar como fazer isso com os")
% (find-2024lean4of0video "10:06" "exemplos dos manuais de Lean")
% (find-2024lean4of0video "10:09" "de um modo que todos os pedaços")
% (find-2024lean4of0video "10:14" "deles ficam visíveis ao mesmo tempo e é")
% (find-2024lean4of0video "10:16" "muito fácil checar detalhes.")

% (find-2024lean4of0video "10:18" "O meu plano é fazer a oficina em")
% (find-2024lean4of0video "10:21" "três aulas só. A primeira aula vai ser")
% (find-2024lean4of0video "10:24" "uma aula sobre instalação do Lean")
% (find-2024lean4of0video "10:26" "e de outras coisas - a gente vai")
% (find-2024lean4of0video "10:29" "usar o Emacs e o eev, mas eu tenho um")
% (find-2024lean4of0video "10:34" "método para instalar eles no no Windows...")

% (find-2024lean4of0video "10:39" "Então, nessa primeira oficina... ela")
% (find-2024lean4of0video "10:43" "demora um pouco, porque alguns passos são")
% (find-2024lean4of0video "10:44" "demorados, mas vocês podem fazer outras")
% (find-2024lean4of0video "10:46" "coisas ao mesmo tempo... vai ter alguns")
% (find-2024lean4of0video "10:48" "momentos em que")
% (find-2024lean4of0video "10:50" "a gente vai ver que o computador vai")
% (find-2024lean4of0video "10:52" "passar 20 ou 30 minutos instalando")
% (find-2024lean4of0video "10:54" "alguma coisa, aí vocês vão fazer outra")
% (find-2024lean4of0video "10:57" "coisa, e quando voltarem tá tudo")
% (find-2024lean4of0video "10:58" "instalado.")

% (find-2024lean4of0video "11:00" "Depois que tiver tudo instalado a gente")
% (find-2024lean4of0video "11:02" "vai poder usar esse tipo de hiperlink")
% (find-2024lean4of0video "11:04" "daqui pra ir pros manuais principais.")

% (find-2024lean4of0video "11:06" "Então: o Lean tem cinco manuais principais.")
% (find-2024lean4of0video "11:10" "Por exemplo esse aqui vai pro Functional")
% (find-2024lean4of0video "11:13" "Programing in Lean, pra uma seção dele que é a")
% (find-2024lean4of0video "11:16" "introdução dele... e ele abre esse manual")
% (find-2024lean4of0video "11:19" "no browser. Então, repara: isso aqui é o")
% (find-2024lean4of0video "11:22" "título do manual, \"Functional Programing...\",")
% (find-2024lean4of0video "11:25" "aqui tem o índice, e a gente abriu a")
% (find-2024lean4of0video "11:27" "introdução...")

% (find-2024lean4of0video "11:29" "e aqui tem um outro manual que é")
% (find-2024lean4of0video "11:32" "o \"Lean Manual\",")
% (find-2024lean4of0video "11:35" "aqui tem o \"Metaprograming in Lean4\",")
% (find-2024lean4of0video "11:39" "aqui tem o \"Type Checking in Lean 4\",")
% (find-2024lean4of0video "11:43" "que é super técnico mas acho que os")
% (find-2024lean4of0video "11:46" "matemáticos vão ter algumas dúvidas que")
% (find-2024lean4of0video "11:48" "vão ser respondidas aqui, e aqui tem")
% (find-2024lean4of0video "11:51" "o \"Theorem Proving in Lean4\", que é um dos")
% (find-2024lean4of0video "11:56" "mais básicos.")

% (find-2024lean4of0video "11:58" "E... a coisa que eu mais gosto no Emacs")
% (find-2024lean4of0video "12:02" "é que dá para criar hiperlinks para tudo")
% (find-2024lean4of0video "12:06" "e os hiperlinks são esses programinhas")
% (find-2024lean4of0video "12:08" "de uma linha em Emacs Lisp. E eu")
% (find-2024lean4of0video "12:11" "já dei um montão de oficinas sobre isso,")
% (find-2024lean4of0video "12:13" "já melhorei meu material sobre isso")
% (find-2024lean4of0video "12:15" "bastante, hoje em dia as pessoas acham")
% (find-2024lean4of0video "12:17" "super fácil de aprender.")

% (find-2024lean4of0video "12:19" "Então aqui tem um exemplo mais exótico.")
% (find-2024lean4of0video "12:22" "É um hiperlink que vai abrir um vídeo numa")
% (find-2024lean4of0video "12:25" "determinada posição. Esse vídeo é")
% (find-2024lean4of0video "12:27" "espetacular - é um vídeo que foi feito há")
% (find-2024lean4of0video "12:28" "poucas semanas atrás...")

% (find-2024lean4of0video "12:32" "sobre... bom deixa eu ver o título dele...")
% (find-2024lean4of0video "12:36" "eu esqueci o título. Vou fazer isso")
% (find-2024lean4of0video "12:41" "aqui... é alguma coisa como")
% (find-2024lean4of0video "12:44" "\"Visualizing Proofs in Lean using Blender\".")

% (find-2024lean4of0video "12:47" "Então é um cara que usa Lean para")
% (find-2024lean4of0video "12:51" "gerar código que usa o Blender")
% (find-2024lean4of0video "12:54" "para fazer animações... é muito")
% (find-2024lean4of0video "12:55" "impressionante. E nesse trecho daqui, a")
% (find-2024lean4of0video "12:59" "partir do 6:50, ele")
% (find-2024lean4of0video "13:05" "mostra como é que ele estendeu a")
% (find-2024lean4of0video "13:07" "linguagem do Lean pra ela reconhecer")
% (find-2024lean4of0video "13:10" "essas posições do jogo de xadrez aqui em")
% (find-2024lean4of0video "13:13" "caracteres Unicode...")

% (find-2024lean4of0video "13:20" "E aí o programa")
% (find-2024lean4of0video "13:22" "dele faz coisas tipo demonstrar que uma")
% (find-2024lean4of0video "13:24" "determinada posição é um mate em cinco")
% (find-2024lean4of0video "13:26" "jogadas, e")
% (find-2024lean4of0video "13:29" "ele pega a prova que é gerada pelo Lean e")
% (find-2024lean4of0video "13:32" "anima ela usando Blender.")

% (find-2024lean4of0video "13:35" "Então dá para fazer esse tipo de")
% (find-2024lean4of0video "13:36" "coisa. É difícil, né, mas já faz a gente")
% (find-2024lean4of0video "13:40" "ter bastante vontade de aprender o Lean...")
% (find-2024lean4of0video "13:42" "é o que eu tô tentando fazer agora.")

% (find-2024lean4of0video "13:44" "Aqui tem um programa relativamente")
% (find-2024lean4of0video "13:47" "básico, que eu fiz... opa, peraí,")
% (find-2024lean4of0video "13:53" "caramba... ah tá, faltou isso.")

% (find-2024lean4of0video "13:57" "Então, esse programa daqui chama uma")
% (find-2024lean4of0video "14:01" "biblioteca que eu fiz... e deixa eu")
% (find-2024lean4of0video "14:04" "primeiro mostrar uma coisa...")
% (find-2024lean4of0video "14:06" "Ah, peraí, deixa eu só fazer uma")
% (find-2024lean4of0video "14:08" "coisinha aqui...")

% (find-2024lean4of0video "14:12" "Pronto. Uma coisa muito legal da")
% (find-2024lean4of0video "14:14" "interface do Lean é que a gente tem duas")
% (find-2024lean4of0video "14:16" "teclas, que eu vou chamar de \"go to\" e")
% (find-2024lean4of0video "14:19" "\"go back\". Por exemplo, se eu tou com")
% (find-2024lean4of0video "14:22" "cursor aqui, em cima desse \"LuaTree\" aqui,")
% (find-2024lean4of0video "14:26" "e aperto a tecla de \"go to\" ele vai")
% (find-2024lean4of0video "14:29" "pro arquivo LuaTree.lean; se eu aperto a tecla")
% (find-2024lean4of0video "14:33" "de \"go back\" ele volta para cá.")

% (find-2024lean4of0video "14:37" "Além disso o Lean tem esse tipo de")
% (find-2024lean4of0video "14:41" "comando daqui, que gera uma")
% (find-2024lean4of0video "14:44" "mensagem aqui na \"echo area\"...")
% (find-2024lean4of0video "14:46" "deixa eu diminuir a fonte... em alguns")
% (find-2024lean4of0video "14:50" "casos a mensagem é bem grande e eu")
% (find-2024lean4of0video "14:53" "também posso pedir para ele mostrar")
% (find-2024lean4of0video "14:54" "todas as mensagens de uma vez.")

% (find-2024lean4of0video "14:56" "Então se eu bato f10 l l - opa, peraí,")
% (find-2024lean4of0video "14:59" "não era isso...")
% (find-2024lean4of0video "15:02" "se eu bato uma sequência misteriosa")
% (find-2024lean4of0video "15:06" "de teclas ele mostra todas as mensagens")
% (find-2024lean4of0video "15:08" "de uma vez...")
% (find-2024lean4of0video "15:10" "e se eu passeio por várias linhas ele dá")
% (find-2024lean4of0video "15:13" "um highlight na mensagem correspondente")
% (find-2024lean4of0video "15:14" "à linha em que eu tou.")

% (find-2024lean4of0video "15:19" "E essa última...")
% (find-2024lean4of0video "15:22" "bom, aqui nesse programa eu defini")
% (find-2024lean4of0video "15:24" "uma linguagenzinha que entende só as")
% (find-2024lean4of0video "15:27" "operações \"-\" e \"^\" e números,")
% (find-2024lean4of0video "15:33" "e a linguagem entende elas com a")
% (find-2024lean4of0video "15:36" "precedência certa.")

% (find-2024lean4of0video "15:37" "Então por exemplo, essa linha daqui")
% (find-2024lean4of0video "15:39" "entende essa expressão daqui e")
% (find-2024lean4of0video "15:41" "parentesisa ela de uma determinada")
% (find-2024lean4of0video "15:44" "forma... essa aqui faz algo parecido mas")
% (find-2024lean4of0video "15:47" "ela produz uma coisa num formato que")
% (find-2024lean4of0video "15:50" "agora não quero explicar, e essa última")
% (find-2024lean4of0video "15:52" "pega essa coisa no formato complicado")
% (find-2024lean4of0video "15:53" "transforma ela numa árvore em 2D.")

% (find-2024lean4of0video "15:56" "Tá, então eu tou mais ou menos nesse nível...")
% (find-2024lean4of0video "15:58" "eu tou aprendendo fazer linguagens muito")
% (find-2024lean4of0video "16:01" "simples, e eu tou tentando entender como é")
% (find-2024lean4of0video "16:03" "que comandos do Lean são")
% (find-2024lean4of0video "16:06" "definidos usando esse método...")
% (find-2024lean4of0video "16:11" "o Lean começa com uma linguagem muito")
% (find-2024lean4of0video "16:14" "básica e depois ele define um montão")
% (find-2024lean4of0video "16:17" "de extensões escritas em Lean mesmo.")

% (find-2024lean4of0video "16:21" "Então, vamos voltar...")
% (find-2024lean4of0video "16:24" "eu tava aqui...")
% (find-2024lean4of0video "16:27" "isso foi só uma demonstração.")

% (find-2024lean4of0video "16:31" "Na primeira aula a gente vai aprender a")
% (find-2024lean4of0video "16:33" "interface do Lean, que eu já mostrei")
% (find-2024lean4of0video "16:35" "algumas coisas dela, e a gente vai")
% (find-2024lean4of0video "16:37" "aprender uma outra coisa bacana que a")
% (find-2024lean4of0video "16:38" "gente pode fazer no Emacs: a gente pode")
% (find-2024lean4of0video "16:41" "acessar o meu conjunto de anotações")
% (find-2024lean4of0video "16:44" "sobre Lean.")

% (find-2024lean4of0video "16:46" "Por exemplo, esse link aqui")
% (find-2024lean4of0video "16:47" "vai pro bloco sobre \"coerção\", que tá aqui...")
% (find-2024lean4of0video "16:51" "toda essa parte aqui tem links")
% (find-2024lean4of0video "16:53" "para documentação, sendo que alguns links")
% (find-2024lean4of0video "16:56" "são um pouco mais estranhos... esse link")
% (find-2024lean4of0video "16:57" "daqui é um link pro resultado de um grep:")
% (find-2024lean4of0video "16:59" "ele vai procurar todas as")
% (find-2024lean4of0video "17:03" "ocorrências disso aqui no código fonte")
% (find-2024lean4of0video "17:05" "das bibliotecas básicas do Lean")
% (find-2024lean4of0video "17:11" "e vai mostrar elas na tela... tá, então")
% (find-2024lean4of0video "17:14" "quando eu tava aprendendo sobre coerção")
% (find-2024lean4of0video "17:16" "eu usei esse tipo de coisa, e esses links")
% (find-2024lean4of0video "17:19" "pro grep vão ser super úteis, e eu vou")
% (find-2024lean4of0video "17:21" "mostrar porquê.")

% (find-2024lean4of0video "17:22" "Então essas são as minhas")
% (find-2024lean4of0video "17:23" "notas sobre coerção, e isso aqui é um")
% (find-2024lean4of0video "17:27" "bloquinho, um snippet [de código Lean]...")

% (find-2024lean4of0video "17:29" "se eu rodo esse comando")
% (find-2024lean4of0video "17:31" "daqui ele abre o meu arquivo temporário")
% (find-2024lean4of0video "17:34" "aqui à direita... deixa eu apagar o")
% (find-2024lean4of0video "17:37" "conteúdo dele...")

% (find-2024lean4of0video "17:39" "e ele bota isso aqui no clipboard do Emacs.")
% (find-2024lean4of0video "17:43" "Aí eu posso ir para cá, bater a tecla de")
% (find-2024lean4of0video "17:46" "\"copy\" e ele copia essas coisas aqui pro")
% (find-2024lean4of0video "17:50" "meu arquivo de teste,")
% (find-2024lean4of0video "17:54" "e aí eu posso examinar o resultado")
% (find-2024lean4of0video "17:56" "de cada coisa dessas.")

% (find-2024lean4of0video "17:58" "Esse \"#check\" aqui ele pega esse termo daqui")
% (find-2024lean4of0video "17:59" "e faz algumas expansões nele...")

% (find-2024lean4of0video "18:03" "então: o \"+\" em")
% (find-2024lean4of0video "18:06" "princípio não sabe somar um número")
% (find-2024lean4of0video "18:08" "natural, que é esse 2, com um inteiro...")

% (find-2024lean4of0video "18:11" "mas na verdade esse \"+\" daqui é")
% (find-2024lean4of0video "18:12" "transformado num \"'+' heterogêneo\",")
% (find-2024lean4of0video "18:15" "que pode receber objetos de dois tipos")
% (find-2024lean4of0video "18:17" "diferentes, e se for necessário ele")
% (find-2024lean4of0video "18:19" "aplica uma coerção em algum deles.")

% (find-2024lean4of0video "18:22" "Então quando a gente pede pro #check mostrar")
% (find-2024lean4of0video "18:24" "que termo é esse daqui ele mostra o termo")
% (find-2024lean4of0video "18:25" "ligeiramente transformado, e mostra que o 2")
% (find-2024lean4of0video "18:28" "recebeu um operador de coerção, aqui...")

% (find-2024lean4of0video "18:30" "a gente também pode examinar")
% (find-2024lean4of0video "18:34" "versões mais detalhadas disso e")
% (find-2024lean4of0video "18:36" "descobrir exatamente qual coerção é")
% (find-2024lean4of0video "18:38" "usada nesse ponto.")

% (find-2024lean4of0video "18:40" "Aí aqui tem um exemplo muito pequeno,")
% (find-2024lean4of0video "18:42" "muito menor do que os do manual...")
% (find-2024lean4of0video "18:43" "de eu definindo dois tipos diferentes")
% (find-2024lean4of0video "18:48" "e definindo uma coerção entre eles...")
% (find-2024lean4of0video "18:51" "e aqui tem vários testes, tá, que eu não vou")
% (find-2024lean4of0video "18:53" "detalhar agora.")

% (find-2024lean4of0video "18:54" "Então, isso é só um exemplo de como as minhas")
% (find-2024lean4of0video "18:57" "anotações têm hiperlinks e têm snippets.")
% (find-2024lean4of0video "19:01" "Deixa eu voltar...")

% (find-2024lean4of0video "19:03" "É isso que a gente vai aprender na primeira aula.")
% (find-2024lean4of0video "19:05" "Então, na primeira aula a gente vai aprender")
% (find-2024lean4of0video "19:07" "a acessar os manuais principais,")
% (find-2024lean4of0video "19:09" "vai aprender o básico da interface,")
% (find-2024lean4of0video "19:10" "vai aprender a apontar")
% (find-2024lean4of0video "19:14" "pra posições de vídeos,")
% (find-2024lean4of0video "19:19" "e a testar código que já existe...")
% (find-2024lean4of0video "19:21" "por exemplo, os meus snippets.")

% (find-2024lean4of0video "19:23" "Aí... eu acho que isso é o que cabe")
% (find-2024lean4of0video "19:27" "na cabeça das pessoas na primeira aula.")
% (find-2024lean4of0video "19:29" "Depois vai estar todo mundo cansado, e uma")
% (find-2024lean4of0video "19:32" "semana depois a gente faz a aula 2, em")
% (find-2024lean4of0video "19:35" "que a gente vai aprender as coisas")
% (find-2024lean4of0video "19:37" "básicas da linguagem - que estão")
% (find-2024lean4of0video "19:39" "explicadas num dos manuais do Lean, o")
% (find-2024lean4of0video "19:42" "\"Functional Programming in Lean\".")

% (find-2024lean4of0video "19:44" "Então a gente vai começar nessa")
% (find-2024lean4of0video "19:46" "seção daqui,")
% (find-2024lean4of0video "19:48" "\"1.1 Evaluating Expressions\", e vai")
% (find-2024lean4of0video "19:52" "possivelmente até a seção 1.5, e eu vou")
% (find-2024lean4of0video "19:55" "traduzir... mostrar para vocês")
% (find-2024lean4of0video "19:59" "as minhas traduções de várias dessas")
% (find-2024lean4of0video "20:01" "demonstrações [?] daqui, por exemplo isso...")

% (find-2024lean4of0video "20:06" "o manual mostra vários trechinhos de")
% (find-2024lean4of0video "20:08" "código - deixa encontrar um interessante...")

% (find-2024lean4of0video "20:11" "e aí por exemplo eu juntei todos os")
% (find-2024lean4of0video "20:14" "trechinho sobre structures num bloco só,")
% (find-2024lean4of0video "20:17" "mostrei várias comparações entre várias")
% (find-2024lean4of0video "20:20" "sintaxes possíveis, fiz um exemplo muito")
% (find-2024lean4of0video "20:22" "mais simples que esse, e tal... então a")
% (find-2024lean4of0video "20:25" "gente vai ver como testar isso...")

% (find-2024lean4of0video "20:27" "e a gente vai considerar que os manuais")
% (find-2024lean4of0video "20:29" "do Lean são a fonte definitiva,")
% (find-2024lean4of0video "20:30" "escrita por pessoas que têm muita prática")
% (find-2024lean4of0video "20:33" "em didática, só que")
% (find-2024lean4of0video "20:36" "elas estão em países em que o ensino é")
% (find-2024lean4of0video "20:40" "muito melhor, em que eles têm")
% (find-2024lean4of0video "20:43" "turmas enormes em que pessoas estão")
% (find-2024lean4of0video "20:45" "aprendendo essas coisas, e tal...")

% (find-2024lean4of0video "20:47" "é o contrário da situação em que eu tou,")
% (find-2024lean4of0video "20:49" "eu tou totalmente isolado, trabalhando num")
% (find-2024lean4of0video "20:51" "campus muito lixo da UFF no interior do")
% (find-2024lean4of0video "20:54" "Estado do Rio de Janeiro...")

% (find-2024lean4of0video "21:00" "Então, outra coisa que a gente vai ver é")
% (find-2024lean4of0video "21:02" "uma coisa que os livros apresentam num")
% (find-2024lean4of0video "21:05" "formato bem difícil - eles dão exercícios")
% (find-2024lean4of0video "21:08" "bem difíceis...")

% (find-2024lean4of0video "21:10" "Eu imagino que todo mundo queira")
% (find-2024lean4of0video "21:12" "aprender um pouquinho sobre")
% (find-2024lean4of0video "21:14" "como usar Lean como")
% (find-2024lean4of0video "21:16" "proof assistant...")

% (find-2024lean4of0video "21:19" "Então a gente vai começar com um exemplo muito")
% (find-2024lean4of0video "21:21" "simples... eu prefiro explicar Curry-Howard")
% (find-2024lean4of0video "21:25" "a partir desse exemplo simples daqui, que")
% (find-2024lean4of0video "21:26" "só usa implicação e...")

% (find-2024lean4of0video "21:28" "Peraí, vamos começar por aqui,")
% (find-2024lean4of0video "21:31" "que é a versão em Dedução Natural dele.")

% (find-2024lean4of0video "21:33" "então, isso aqui é o \"e\". Se eu sei que")
% (find-2024lean4of0video "21:37" "P∧R é verdade eu sei que P é verdade,")
% (find-2024lean4of0video "21:40" "se eu sei que P é verdade e P→Q é")
% (find-2024lean4of0video "21:42" "verdade eu sei que Q é verdade...")

% (find-2024lean4of0video "21:45" "Então, aqui tem a tradução dessa")
% (find-2024lean4of0video "21:48" "demonstração simples em dedução")
% (find-2024lean4of0video "21:50" "natural para uma demonstração em")
% (find-2024lean4of0video "21:53" "conjuntos... então isso para mim é o")
% (find-2024lean4of0video "21:55" "primeiro exemplo interessante de")
% (find-2024lean4of0video "21:57" "Curry-Howard...")

% (find-2024lean4of0video "21:59" "E aqui à esquerda a gente diz qual é o")
% (find-2024lean4of0video "22:02" "elemento do conjunto se eu conheço um")
% (find-2024lean4of0video "22:04" "elemento desse conjunto A'×B daqui -")
% (find-2024lean4of0video "22:06" "o elemento p - então a primeira projeção,")
% (find-2024lean4of0video "22:11" "πp, vai ser um elemento desse conjunto")
% (find-2024lean4of0video "22:12" "daqui, A'.")

% (find-2024lean4of0video "22:14" "Eu acho que essa notação daqui é")
% (find-2024lean4of0video "22:17" "a notação mais familiar para")
% (find-2024lean4of0video "22:20" "matemáticos, e a gente vai ver")
% (find-2024lean4of0video "22:24" "que o Lean costuma usar uma convenção que")
% (find-2024lean4of0video "22:27" "para mim é estranha - é uma convenção")
% (find-2024lean4of0video "22:29" "usada pelo pessoal de linguagens")
% (find-2024lean4of0video "22:31" "funcionais...")

% (find-2024lean4of0video "22:35" "deixa eu pegar uma figura aqui...")
% (find-2024lean4of0video "22:35" "aqui é um outro trecho daquele")
% (find-2024lean4of0video "22:39" "vídeo que eu falei que é maravilhoso...")

% (find-2024lean4of0video "22:44" "Em geral a gente quer aprender o Lean")
% (find-2024lean4of0video "22:48" "como provador de teoremas")
% (find-2024lean4of0video "22:50" "começando por \"táticas\".")

% (find-2024lean4of0video "22:52" "Muita gente começa rodando o Lean")
% (find-2024lean4of0video "22:54" "no browser, no tal do")
% (find-2024lean4of0video "22:56" "\"Natural Numbers Game\" e aí aquilo é um")
% (find-2024lean4of0video "23:00" "tutorial que já começa direto por táticas.")

% (find-2024lean4of0video "23:02" "O meu primeiro contato com Lean")
% (find-2024lean4of0video "23:04" "foi no meio da pandemia quando um cara")
% (find-2024lean4of0video "23:05" "chamado Francesco Noseda, que é um professor")
% (find-2024lean4of0video "23:11" "da UFRJ... ele deu um curso de Lean online")
% (find-2024lean4of0video "23:15" "e eu participei, e no curso dele ele supunha")
% (find-2024lean4of0video "23:18" "que as pessoas sabiam um bocado")
% (find-2024lean4of0video "23:21" "sobre técnicas de demonstração em")
% (find-2024lean4of0video "23:24" "Cálculo de Sequentes e Fitch, e apesar")
% (find-2024lean4of0video "23:28" "que eu trabalho com Lógica a minha")
% (find-2024lean4of0video "23:29" "formação é muito estranha - eu nunca tive")
% (find-2024lean4of0video "23:31" "um curso formal disso...")

% (find-2024lean4of0video "23:33" "então, eu sou meio ruim nessas coisas...")
% (find-2024lean4of0video "23:35" "eu sou bom em Dedução Natural,")
% (find-2024lean4of0video "23:37" "mas eu tenho pouca prática com")
% (find-2024lean4of0video "23:38" "técnicas de demonstração, Cálculo de")
% (find-2024lean4of0video "23:40" "Sequentes, coisas assim")
% (find-2024lean4of0video "23:42" "formalizadas do jeito tradicional para")
% (find-2024lean4of0video "23:46" "quem fez um curso de Lógica.")

% (find-2024lean4of0video "23:49" "Então, eu ralei muito pra")
% (find-2024lean4of0video "23:51" "entender aquilo, e eu fiquei com a sensação")
% (find-2024lean4of0video "23:52" "de que faltavam diagramas. Nesse vídeo eu")
% (find-2024lean4of0video "23:55" "consigo mostrar para vocês que tipo de")
% (find-2024lean4of0video "23:56" "diagrama faltava.")

% (find-2024lean4of0video "23:58" "No curso do Francesco e a gente não")
% (find-2024lean4of0video "24:03" "conseguia... a gente via esse tipo de coisa")
% (find-2024lean4of0video "24:05" "daqui - aqui tem um exemplo de que")
% (find-2024lean4of0video "24:08" "hipóteses a gente tem num certo momento")
% (find-2024lean4of0video "24:12" "e o que que a gente quer provar...")

% (find-2024lean4of0video "24:18" "e nessa figura daqui ele mostra")
% (find-2024lean4of0video "24:21" "que quando a gente roda essa tática daqui")
% (find-2024lean4of0video "24:23" "o nosso conjunto de hipóteses e")
% (find-2024lean4of0video "24:27" "a coisa que a gente quer provar mudam")
% (find-2024lean4of0video "24:29" "desse bloquinho de cima para esse")
% (find-2024lean4of0video "24:31" "bloquinho de baixo.")

% (find-2024lean4of0video "24:32" "Então para mim quando a gente consegue")
% (find-2024lean4of0video "24:35" "ver o \"antes\" e o \"depois\" na mesma")
% (find-2024lean4of0video "24:37" "tela fica muito mais fácil de entender,")
% (find-2024lean4of0video "24:40" "e na época do curso de Francesco ele não")
% (find-2024lean4of0video "24:43" "mostrou isso, ele não tinha técnicas pra")
% (find-2024lean4of0video "24:45" "mostrar isso... e eu passei dias tentando")
% (find-2024lean4of0video "24:48" "fazer as figurinhas para conseguir")
% (find-2024lean4of0video "24:51" "entender quais eram as táticas principais.")

% (find-2024lean4of0video "24:54" "Agora, outro motivo pra gente")
% (find-2024lean4of0video "24:56" "não aprender táticas nesse meu curso de")
% (find-2024lean4of0video "24:58" "três aulas é que mesmo o Theorem Proving")
% (find-2024lean4of0video "25:03" "Lean... deixa eu aumentar a letra de novo...")
% (find-2024lean4of0video "25:06" "ele só ensina táticas no capítulo 5 dele.")

% (find-2024lean4of0video "25:10" "Então, antes ele ensina a Teoria de")
% (find-2024lean4of0video "25:13" "Tipos básica até quantificadores, outros")
% (find-2024lean4of0video "25:16" "modos de demonstrar proposições simples...")
% (find-2024lean4of0video "25:18" "as táticas só aparecem no capítulo 5.")

% (find-2024lean4of0video "25:21" "Então, a gente vai aprender essas")
% (find-2024lean4of0video "25:26" "coisas na aula 2, e na aula 2 eu")
% (find-2024lean4of0video "25:29" "só vou supor que as pessoas sabem um")
% (find-2024lean4of0video "25:31" "pouquinho de Matemática e têm uma noção de")
% (find-2024lean4of0video "25:34" "tipos mesmo que seja de linguagens como C,")
% (find-2024lean4of0video "25:36" "e já tentaram aprender Haskell e")
% (find-2024lean4of0video "25:40" "quebraram a cara...")

% (find-2024lean4of0video "25:40" "que elas têm uma noção de coisas")
% (find-2024lean4of0video "25:43" "mais básicas, mas empacaram -")
% (find-2024lean4of0video "25:45" "possivelmente nos mesmos lugares que eu.")

% (find-2024lean4of0video "25:47" "Então, isso é aula 2, e eu")
% (find-2024lean4of0video "25:51" "suponho que a aula 2 vai")
% (find-2024lean4of0video "25:53" "interessar pra um bocado de gente...")
% (find-2024lean4of0video "25:56" "e a aula 2 é desculpa para as")
% (find-2024lean4of0video "25:58" "pessoas aprenderem a aula 1, e na aula 1")
% (find-2024lean4of0video "26:00" "eu vou apresentar o Emacs e a")
% (find-2024lean4of0video "26:03" "biblioteca que eu fiz pro Emacs, que é")
% (find-2024lean4of0video "26:05" "essa biblioteca de hiperlinks e outras")
% (find-2024lean4of0video "26:07" "coisas, que é o eev.")

% (find-2024lean4of0video "26:10" "A aula 3 eu ainda não preparei o")
% (find-2024lean4of0video "26:14" "material dela direito, e ela é bem mais")
% (find-2024lean4of0video "26:16" "avançada... eu não sei quanta gente")
% (find-2024lean4of0video "26:18" "vai se interessar por ela,")
% (find-2024lean4of0video "26:21" "porque tem bem pouca gente no Brasil que")
% (find-2024lean4of0video "26:24" "se interessa por linguagens funcionais, e")
% (find-2024lean4of0video "26:27" "até onde eu sei a maioria das pessoas")
% (find-2024lean4of0video "26:28" "que se interessam por linguagens funcionais")
% (find-2024lean4of0video "26:30" "está super sem tempo, então eu não sei")
% (find-2024lean4of0video "26:33" "quantas pessoas vão fazer")
% (find-2024lean4of0video "26:35" "esse meu minicurso...")

% (find-2024lean4of0video "26:38" "e na verdade para mim o mínimo é 1 -")
% (find-2024lean4of0video "26:41" "se tiver uma pessoa interessada e for uma")
% (find-2024lean4of0video "26:42" "pessoa animada, que tem coragem de dizer")
% (find-2024lean4of0video "26:45" "\"eu não entendi isso aqui\" quando eu mostrar")
% (find-2024lean4of0video "26:47" "um determinado exemplo, para mim já tá bom...")
% (find-2024lean4of0video "26:49" "porque eu consigo testar esse material e")
% (find-2024lean4of0video "26:53" "transformar ele num blog post grande, em")
% (find-2024lean4of0video "26:56" "alguma coisa publicável, sei lá...")

% (find-2024lean4of0video "27:00" "então, digamos que a aula 3 interesse")
% (find-2024lean4of0video "27:02" "para bem menos gente, e pode ser que")
% (find-2024lean4of0video "27:05" "algumas pessoas assistam a aula 3 mais por")
% (find-2024lean4of0video "27:11" "curiosidade mas achem tudo muito avançado...")

% (find-2024lean4of0video "27:14" "Basicamente na aula 3 a gente vai ver")
% (find-2024lean4of0video "27:16" "as figuras que me salvaram")
% (find-2024lean4of0video "27:18" "para entender várias coisas do Lean.")

% (find-2024lean4of0video "27:20" "Aqui tem um exemplo dessas figuras...")
% (find-2024lean4of0video "27:24" "ih, não, tou na página errada, deixa eu ir")
% (find-2024lean4of0video "27:28" "pra outra página... tá aqui.")

% (find-2024lean4of0video "27:32" "Por exemplo, isso aqui é um exemplo de")
% (find-2024lean4of0video "27:36" "mônadas sem usar a notação \"do\", que vou")
% (find-2024lean4of0video "27:40" "supor que vocês já ouviram falar. Então,")
% (find-2024lean4of0video "27:43" "isso aqui é um exemplinho de mônadas com")
% (find-2024lean4of0video "27:45" "a notação \"do\" traduzida pra uma notação")
% (find-2024lean4of0video "27:47" "mais básica e com as anotações de tipos.")

% (find-2024lean4of0video "27:50" "E pra mim tinha umas coisas que eram")
% (find-2024lean4of0video "27:52" "super misteriosas, que é... por exemplo,")
% (find-2024lean4of0video "27:54" "como é que a gente descobre que uma")
% (find-2024lean4of0video "27:56" "operação dessas, que usa a mônada")
% (find-2024lean4of0video "27:59" "de listas retorna uma lista?")

% (find-2024lean4of0video "28:03" "E aí a gente tem que fazer")
% (find-2024lean4of0video "28:06" "essas type inferences todas pra entender")
% (find-2024lean4of0video "28:09" "como é que esse \"bind\" vai funcionar,")
% (find-2024lean4of0video "28:14" "porque tem que ser o bind \"da mônada")
% (find-2024lean4of0video "28:16" "associada a isso aqui\" e aí esse bind")
% (find-2024lean4of0video "28:19" "determina qual vai ser o \"pure\", e o pure")
% (find-2024lean4of0video "28:22" "vai fazer com que o resultado seja uma")
% (find-2024lean4of0video "28:24" "lista de pares do tipo A×B...")

% (find-2024lean4of0video "28:26" "então eu")
% (find-2024lean4of0video "28:28" "ficava lendo os capítulos sobre")
% (find-2024lean4of0video "28:32" "mônadas dos tutoriais, eles davam um")
% (find-2024lean4of0video "28:34" "montão de exemplos de uso, um montão de")
% (find-2024lean4of0video "28:36" "analogias... e nada fazia muito sentido pra")
% (find-2024lean4of0video "28:38" "mim, e a partir do momento em que eu")
% (find-2024lean4of0video "28:40" "consegui ver todos esses detalhes")
% (find-2024lean4of0video "28:42" "tudo ficou muito mais claro. Então eu vou")
% (find-2024lean4of0video "28:44" "apresentar isso e a gente vai discutir e")
% (find-2024lean4of0video "28:48" "eu vou tentar descobrir se esse tipo de")
% (find-2024lean4of0video "28:49" "coisa ajuda outras pessoas também, ou não...")

% (find-2024lean4of0video "28:53" "Aqui tem um outro exemplo de coisa...")
% (find-2024lean4of0video "28:56" "de figura que me ajudou muito.")
% (find-2024lean4of0video "28:58" "Deixa eu pegar esse pedacinho dela.")

% (find-2024lean4of0video "29:05" "Vamos olhar só pra parte de cima dela.")
% (find-2024lean4of0video "29:08" "Isso aqui é uma função que recebe")
% (find-2024lean4of0video "29:13" "esses argumentos implícitos aqui, então o")
% (find-2024lean4of0video "29:15" "usuário não precisa dar esses argumentos,")
% (find-2024lean4of0video "29:17" "o Lean vai inferir esses argumentos")
% (find-2024lean4of0video "29:19" "a partir do resto...")

% (find-2024lean4of0video "29:23" "Aí tem essa coisa muito misteriosa aqui,")
% (find-2024lean4of0video "29:25" "que eu levei meses para entender, e aí")
% (find-2024lean4of0video "29:27" "tem essa coisa um pouco mais clara aqui...")
% (find-2024lean4of0video "29:29" "aqui a gente tem o produto dos dois")
% (find-2024lean4of0video "29:31" "tipos, que a gente pode considerar que é um")
% (find-2024lean4of0video "29:32" "produto cartesiano de dois conjuntos, e")
% (find-2024lean4of0video "29:35" "um ponto desse produto cartesiano.")

% (find-2024lean4of0video "29:37" "Aqui tem uma coisa invisível...")

% (find-2024lean4of0video "29:41" "e aí essa função que recebe esses")
% (find-2024lean4of0video "29:44" "argumentos vai retornar o resultado")
% (find-2024lean4of0video "29:45" "dessa coisa daqui aqui.")

% (find-2024lean4of0video "29:47" "Tem uma expressão que vai pegar esse ab,")
% (find-2024lean4of0video "29:48" "que é um par, vai separar ele")
% (find-2024lean4of0video "29:52" "em lado esquerdo e lado direito,")
% (find-2024lean4of0video "29:54" "vai colocar o lado esquerdo")
% (find-2024lean4of0video "29:56" "dentro da variável a e vai ignorar o lado")
% (find-2024lean4of0video "29:58" "direito... e aí aqui à direita a gente vai")
% (find-2024lean4of0video "30:00" "retornar o resultado disso.")

% (find-2024lean4of0video "30:03" "E aí como é que a gente faz pra")
% (find-2024lean4of0video "30:05" "entender uma coisa dessas?")

% (find-2024lean4of0video "30:08" "Eu descobri que o melhor modo de entender")
% (find-2024lean4of0video "30:10" "essas coisas é a gente olhar pro parser")
% (find-2024lean4of0video "30:12" "do Lean.")

% (find-2024lean4of0video "30:15" "Então a gente vai dar uma olhada em como")
% (find-2024lean4of0video "30:20" "cada estrutura sintática é definida lá...")
% (find-2024lean4of0video "30:23" "algumas têm comentários bem interessantes,")
% (find-2024lean4of0video "30:25" "outras têm só referências e outras coisas")
% (find-2024lean4of0video "30:27" "[?] que mais ou menos legível")

% (find-2024lean4of0video "30:29" "E aí eu fui")
% (find-2024lean4of0video "30:30" "descobrindo que essa coisa aqui era")
% (find-2024lean4of0video "30:34" "uma \"typeAscription\", essa coisa")
% (find-2024lean4of0video "30:36" "misteriosa daqui era um \"instance binder\",")
% (find-2024lean4of0video "30:39" "e a partir do nome [?] que eu descobri isso")
% (find-2024lean4of0video "30:40" "eu consegui descobrir quais seções do")
% (find-2024lean4of0video "30:42" "manual explicavam essas coisas... e aí aos")
% (find-2024lean4of0video "30:46" "pouquinhos tudo foi ficando claro.")

% (find-2024lean4of0video "30:49" "Essa figura daqui pode ser dividida")
% (find-2024lean4of0video "30:51" "em figuras que detalham...")
% (find-2024lean4of0video "30:53" "bom, eu não consegui fazer um")
% (find-2024lean4of0video "30:56" "parsing diagram que coubesse numa linha só,")
% (find-2024lean4of0video "31:01" "ficava muito grande, então eu dividi")
% (find-2024lean4of0video "31:02" "isso em vários...")

% (find-2024lean4of0video "31:02" "por exemplo, esse {α β} entre chaves aqui")
% (find-2024lean4of0video "31:08" "ele pode ser transformado")
% (find-2024lean4of0video "31:12" "nessa árvore daqui, bem maior...")

% (find-2024lean4of0video "31:14" "isso aqui é parseado pelo \"implicitBinder\"...")

% (find-2024lean4of0video "31:18" "essa outra estrutura daqui")
% (find-2024lean4of0video "31:21" "é parseada pelo instBinder...")

% (find-2024lean4of0video "31:28" "e essa última daqui é parseada")
% (find-2024lean4of0video "31:32" "desse jeito daqui...")
% (find-2024lean4of0video "31:33" "e o \"let\" é parseado por essas duas")
% (find-2024lean4of0video "31:38" "árvores daqui de baixo.")

% (find-2024lean4of0video "31:40" "Tá, então a gente vai entender isso aqui,")
% (find-2024lean4of0video "31:44" "que é um outro tipo de diagrama")
% (find-2024lean4of0video "31:45" "que me salvou...")

% (find-2024lean4of0video "31:48" "E... ai caramba... aqui.")
% (find-2024lean4of0video "31:58" "E basicamente é isso.")
% (find-2024lean4of0video "32:01" "Talvez tenha um outro tipo de")
% (find-2024lean4of0video "32:04" "diagrama, que é pra gente entender o que")
% (find-2024lean4of0video "32:07" "que é um \"Pratt parser\" e como é que o")
% (find-2024lean4of0video "32:11" "Lean entende precedência, macros e outras")
% (find-2024lean4of0video "32:13" "coisas... mas eu ainda não tenho exemplos")
% (find-2024lean4of0video "32:15" "muito bons dele... então é basicamente isso.")

% (find-2024lean4of0video "32:21" "Tem mais uma seção aqui... peraí.")
% (find-2024lean4of0video "32:28" "Ah, não, era só isso. Eu já expliquei qual")
% (find-2024lean4of0video "32:30" "era minha motivação, meu público alvo, a")
% (find-2024lean4of0video "32:33" "história da didática e tudo mais, e só")
% (find-2024lean4of0video "32:36" "falta falar uma coisa.")

% (find-2024lean4of0video "32:38" "É o seguinte eu já")
% (find-2024lean4of0video "32:39" "disse que eu tou trabalhando num campus")
% (find-2024lean4of0video "32:40" "da UFF que é muito pequeno. Eu já tinha")
% (find-2024lean4of0video "32:43" "uma noção de que esse campus era um lixo,")
% (find-2024lean4of0video "32:45" "até um tempo atrás... mas")
% (find-2024lean4of0video "32:48" "nos últimos do anos eu consegui")
% (find-2024lean4of0video "32:50" "descobrir que ele é um lixo, assim, 10")
% (find-2024lean4of0video "32:52" "vezes maior do que eu pensava...")

% (find-2024lean4of0video "32:55" "não dá para interagir com os meus colegas de lá")
% (find-2024lean4of0video "32:57" "nem mesmo pra discutir os cursos")
% (find-2024lean4of0video "32:59" "que eu tou dando e técnicas de didática...")
% (find-2024lean4of0video "33:02" "e eu oferecia umas oficinas de Software")
% (find-2024lean4of0video "33:03" "Livre pros... basicamente pros alunos,")
% (find-2024lean4of0video "33:07" "e eles não iam nunca, e eu não entendia")
% (find-2024lean4of0video "33:09" "porquê...")

% (find-2024lean4of0video "33:10" "e aí durante a greve eu ofereci")
% (find-2024lean4of0video "33:12" "essas oficinas divulgando elas pro")
% (find-2024lean4of0video "33:14" "pessoal de todos os cursos e eu vi que")
% (find-2024lean4of0video "33:16" "as pessoas de Produção Cultural e")
% (find-2024lean4of0video "33:18" "Psicologia iam nas oficinas, ficavam")
% (find-2024lean4of0video "33:21" "super animadas, faziam milhões")
% (find-2024lean4of0video "33:22" "de perguntas... mas os alunos da")
% (find-2024lean4of0video "33:25" "Computação e da Engenharia - eles não iam")
% (find-2024lean4of0video "33:27" "de jeito nenhum.")

% (find-2024lean4of0video "33:29" "Aí eu fui entendendo aos poucos - até")
% (find-2024lean4of0video "33:31" "porque eu conversei com umas pessoas que")
% (find-2024lean4of0video "33:33" "estudaram em Niterói - que eles têm uma")
% (find-2024lean4of0video "33:36" "mentalidade na qual é inconcebível você")
% (find-2024lean4of0video "33:39" "estudar junto com os colegas, você tirar")
% (find-2024lean4of0video "33:41" "dúvida dos colegas, você ir na oficina")
% (find-2024lean4of0video "33:43" "dos colegas... então eles não tem uma")
% (find-2024lean4of0video "33:47" "mentalidade de \"estamos na universidade")
% (find-2024lean4of0video "33:50" "pública, vamos fazer tudo que aparecer,")
% (find-2024lean4of0video "33:52" "vamos aprender tudo que der, e vamos")
% (find-2024lean4of0video "33:54" "compartilhar o conhecimento\"...")

% (find-2024lean4of0video "33:56" "É uma coisa muito estranha. Eles")
% (find-2024lean4of0video "33:58" "talvez tenham pego um pouco da mentalidade")
% (find-2024lean4of0video "34:00" "do pessoal da Engenharia de Produção, não")
% (find-2024lean4of0video "34:03" "sei direito... mas de qualquer forma é")
% (find-2024lean4of0video "34:07" "péssimo.")

% (find-2024lean4of0video "34:08" "E aí eu tô querendo dar essa oficina")
% (find-2024lean4of0video "34:10" "pra fazer contato com pessoas")
% (find-2024lean4of0video "34:12" "de outras universidades, descobrir que")
% (find-2024lean4of0video "34:13" "que elas estão fazendo, descobrir como é que")
% (find-2024lean4of0video "34:15" "eu posso participar dos projetos delas,")
% (find-2024lean4of0video "34:17" "grudar nelas de alguma forma fazendo")
% (find-2024lean4of0video "34:20" "coisas interessantes junto com elas online...")

% (find-2024lean4of0video "34:23" "Deixa eu só mostrar uma coisinha que faltou.")
% (find-2024lean4of0video "34:26" "Eu mostrei como é que esses")
% (find-2024lean4of0video "34:28" "links daqui vão para seções dos manuais...")
% (find-2024lean4of0video "34:31" "por exemplo, esse aqui abre")
% (find-2024lean4of0video "34:35" "a versão em HTML do")
% (find-2024lean4of0video "34:37" "\"Functional Programing in Lean\"...")

% (find-2024lean4of0video "34:42" "e todos esses manuais exceto um têm")
% (find-2024lean4of0video "34:46" "fonte num formato super fácil de acessar,")
% (find-2024lean4of0video "34:52" "e a gente consegue extrair os")
% (find-2024lean4of0video "34:55" "bloquinhos de código dessa fonte.")

% (find-2024lean4of0video "34:58" "Então, por exemplo, nesse manual")
% (find-2024lean4of0video "35:03" "daqui, do \"Metaprograming\", tem uma seção...")
% (find-2024lean4of0video "35:06" "repara que esse link daqui veio pra uma subseção")
% (find-2024lean4of0video "35:11" "dessa página, a subseção se chama \"Building")
% (find-2024lean4of0video "35:13" "a DSL and a syntax for it\"...")

% (find-2024lean4of0video "35:15" "é um exemplo mais ou menos básico")
% (find-2024lean4of0video "35:16" "de como criar uma linguagenzinha nova...")

% (find-2024lean4of0video "35:21" "e eu também posso ir pro código fonte")
% (find-2024lean4of0video "35:24" "disso aqui, que gerou esse HTML...")

% (find-2024lean4of0video "35:28" "Então, se eu rodo esse hiperlink daqui")
% (find-2024lean4of0video "35:33" "ele abre o código fonte disso...")
% (find-2024lean4of0video "35:35" "repara, esse título aparece")
% (find-2024lean4of0video "35:38" "desse jeito aqui, e esse bloquinho de")
% (find-2024lean4of0video "35:40" "código aparece desse jeito... isso aqui é")
% (find-2024lean4of0video "35:43" "um arquivo em Lean, o arquivo parseou")
% (find-2024lean4of0video "35:46" "essas coisas daqui")
% (find-2024lean4of0video "35:48" "interpretou esse bloquinho daqui como")
% (find-2024lean4of0video "35:52" "Lean, coloriu tudo do jeito certo, e,")
% (find-2024lean4of0video "35:59" "por exemplo... talvez se eu usar a tecla")
% (find-2024lean4of0video "36:01" "de \"go to\" aqui talvez ele vá")
% (find-2024lean4of0video "36:03" "pra definição do \"inductive\"... bom,")
% (find-2024lean4of0video "36:07" "talvez, mas eu não tenho certeza...")

% (find-2024lean4of0video "36:11" "Tudo funciona exatamente como")
% (find-2024lean4of0video "36:14" "naquele outro demo que eu mostrei - cada")
% (find-2024lean4of0video "36:15" "\"#check\" desses mostra um output aqui")
% (find-2024lean4of0video "36:19" "embaixo, e se eu bater f10 l l...")

% (find-2024lean4of0video "36:24" "opa, não, seu eu bater essa")
% (find-2024lean4of0video "36:26" "sequência misteriosa de teclas daqui")
% (find-2024lean4of0video "36:29" "ele mostra todas as mensagens de uma vez.")

% (find-2024lean4of0video "36:32" "Então: a gente vai ver como acessar esse...")
% (find-2024lean4of0video "36:36" "o código fonte, e extrair o código fonte")
% (find-2024lean4of0video "36:40" "e criar arquivos menores com isso, em que")
% (find-2024lean4of0video "36:42" "a gente possa fazer nossos experimentos...")
% (find-2024lean4of0video "36:45" "modificar coisas, simplificar coisas")
% (find-2024lean4of0video "36:47" "acrescentar coisas, etc...")

% (find-2024lean4of0video "36:49" "Então isso é uma coisa que a gente")
% (find-2024lean4of0video "36:51" "vai ver superficialmente na primeira")
% (find-2024lean4of0video "36:53" "aula e depois a gente vai usar")
% (find-2024lean4of0video "36:55" "bastante.")

% (find-2024lean4of0video "36:57" "E... é isso. O vídeo era isso aí.")
% (find-2024lean4of0video "37:01" "Qualquer coisa acessem essas")
% (find-2024lean4of0video "37:04" "páginas pra mais informações e entrem")
% (find-2024lean4of0video "37:07" "em contato comigo... e se vocês tiverem")
% (find-2024lean4of0video "37:09" "algum interesse no curso por")
% (find-2024lean4of0video "37:11" "favor peguem os meus contatos e mandem")
% (find-2024lean4of0video "37:13" "ou e-mail ou mensagem por WhatsApp ou")
% (find-2024lean4of0video "37:16" "por Telegram. É isso por enquanto!")

% (find-2024lean4of0video "37:20" " ")

]==]

unrevised_bigstr = [==[
% (find-2024lean4of0video "00:00" " ")

]==]

-- Local Variables:
-- coding:  utf-8-unix
-- End: