fbanados

OS X Screencast to animated GIF

This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.

Instructions

To capture the video (filesize: 19MB), using the free "QuickTime Player" application:

fbanados

Require Import Coq.NArith.NArith.

Theorem add_1_r : forall p, (p + 1)%positive = Pos.succ p.
Proof.
  induction p; simpl; eauto.
Qed.

Theorem add_carry_spec : forall p q, Pos.add_carry p q = Pos.succ (p + q).
Proof.
  induction p; induction q; simpl; eauto.

fbanados

The --- separator is not squeak syntax, but is presented to distinguish IDE("Browser") code from REPL content ("Workspace").

fbanados

#lang slideshow

(require slideshow/play)

(provide timer-slide)

(module stopwatch racket
  (provide (all-defined-out))
  (define time? number?)
  (define (seconds n) n)

fbanados

(define pipe
  ; Inspired on F#'s Forward pipe operator (|>)
  (lambda args
    (let ((v (car args))
          (functions (cdr args)))
      (foldl (λ (f v) (f v)) v functions))))

(test (pipe 1
            add1

fbanados

brew install ncurses
gem install ncursesw -- --with-opt-dir=/usr/local/opt/ncurses

fbanados

#lang racket

;P1 No. Al evaluar, el nombre 'fibs en la llamada recursiva no se encontrará en el ambiente.

;P3:

;pow no es recursiva por la cola
(define (pow base exp)
  (if (= exp 0)
      1

fbanados

#lang plazy

(define (my-if p t f)
  (if p t f))

(define (infiniteloop x)
  (infiniteloop x))

;al contrario de #lang racket, aquí esta función sí funciona correctamente.
(my-if #f (infiniteloop 0) 123)

fbanados

#lang racket

(define (my-if pred true false)
  (if
   (pred)
   (true)
   (false)))

;(define (infiniteloop x)
;  (infiniteloop x))

fbanados

#lang plai 

#|
<WAE> ::= <num> 
      |  {+ <WAE> <WAE>}
      |  {- <WAE> <WAE>}
      |  {with {<id> <WAE>} <WAE>}
      |  <id>
|#
(define-type WAE