relrod

Theorem iso_comp_iso
        {C : Category}
        {a b c : @ob C}
        (f : Isomorphism a b)
        (g : Isomorphism b c) :
  Isomorphism a c.
Proof.
  destruct f, g.
  exists (comp to0 to1) (comp from1 from0).
  rewrite assoc.

relrod

Program Definition iso_comp_iso
        {C : Category}
        {a b c : C}
        (x : @Isomorphism C a b)
        (y : @Isomorphism C b c) :
  @Isomorphism C a c :=
  {| to := comp (to x) (to y);
     from := comp (from y) (from x)
  |}.
Next Obligation.

relrod

Set Primitive Projections.

Record PointedSet {set : Type} :=
  { basepoint : set
  }.

(** * Point-preserving maps.

Let \((X, x)\) and \((Y, y)\) be pointed sets. Then a point-preserving map
between them is a function \(f : (X, x) \to (Y, y)\). That is, a function from

relrod

module Main where

import Control.Monad.Free

data FizzBuzz a
  = Fizz a
  | Buzz a
  | FizzBuzz a
  | Num Integer a
  deriving (Eq, Ord, Show)

relrod

    if (((m/^\s*(?:'[^']*?'|"[^"]*?"|[^"'#]*?)*?([^"'#<@])<<(\w+)\s*/ &&
          ($2 !~ m/^\d+$/)) ||
         m/^\s*(?:'[^']*?'|"[^"]*?"|[^"'#]*?)*?[^"'#<@]<<\s*(["'`])(.+?|)\1\s*/
        ) &&
         ! m/q[qxwr]?\s*[{([#|!\/][^})\]#|!\/]*?<<[^<]/
       ) {

relrod

diff --git a/fpaste b/fpaste
index 7a2eefe..d33461a 100755
--- a/fpaste
+++ b/fpaste
@@ -20,7 +20,7 @@ VERSION = '0.3.8.1'
 USER_AGENT = 'fpaste/' + VERSION
 SET_DESCRIPTION_IF_EMPTY = 1  # stdin, clipboard, sysinfo
 # FPASTE_URL = 'http://fpaste.org/'
-FPASTE_URL = 'http://paste.fedoraproject.org/'
+FPASTE_URL = 'http://modernpaste.fedorainfracloud.org/api/paste'

relrod

Require Import Ascii String Zdiv.

Open Scope string.

Inductive format :=
| fmt_int : format -> format
| fmt_string : format -> format
| fmt_other : ascii -> format -> format
| fmt_end : format.

relrod

Definition digit_to_string n : string :=
  match n with
  | 0%Z => "0"
  | 1%Z => "1"
  | 2%Z => "2"
  | 3%Z => "3"
  | 4%Z => "4"
  | 5%Z => "5"
  | 6%Z => "6"

relrod

Lemma ap_pres_comp : forall {t u} (pu : parser (t -> u)) (pv : parser (t -> t)) pw,
    ((ret compose <*> pu) <*> pv) <*> pw = pu <*> (pv <*> pw).
Proof.
  intros.
  unfold ap.
  unfold flatmap.
  extensionality x.
  simpl.
  destruct (pu x).
  destruct p.

relrod

     = fun i : string =>
       match
         match
           match i with
           | "" => None
           | String h t => Some (h, t)
           end
         with
         | Some (x, i') =>
             (if