Skip to content

Instantly share code, notes, and snippets.

@peterbb

peterbb/gist:7313499

Last active December 27, 2015 10:48
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save peterbb/7313499 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save peterbb/7313499 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. peterbb revised this gist Nov 5, 2013. 1 changed file with 1 addition and 0 deletions.
    1 change: 1 addition & 0 deletions gistfile1.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -10,4 +10,5 @@ Section TMP.

    Goal (exists f : nat -> A, f 0 = a /\ f 1 = b).
    exists f; auto.
    Qed.
    End TMP.
  2. peterbb created this gist Nov 5, 2013.
    13 changes: 13 additions & 0 deletions gistfile1.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,13 @@
    Section TMP.
    Variable A : Set.
    Variables a b : A.

    Definition f (n : nat) : A :=
    match n with
    | 0 => a
    | _ => b
    end.

    Goal (exists f : nat -> A, f 0 = a /\ f 1 = b).
    exists f; auto.
    End TMP.