vikraman

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

infixr 20 _∷_

data M {ℓ} (A : Type ℓ) : Type ℓ where

vikraman

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)

vikraman

(** * Stlc: Functorial semantics of STLC (McBride) *)

(** Coq programmers usually avoid using dependent types, because
    dependent pattern matching is difficult to use. However, with a
    principled use of the induction principle and using refine/eapply,
    dependently typed programming in Coq can be made enjoyable. *)

Module Stlc.

Inductive Ty : Type :=

vikraman

{-# OPTIONS --type-in-type #-}

module Yoneda where

_∘_ : {a b c : Set} → (b → c) → (a → b) → (a → c)
f ∘ g = λ z → f (g z)

record Functor (f : Set → Set) : Set where
  field
    map : {a b : Set} → (a → b) → f a → f b

vikraman

Keybase proof

I hereby claim:

• I am vikraman on github.
• I am vikraman (https://keybase.io/vikraman) on keybase.
• I have a public key whose fingerprint is CE52 ABDA 543E 4957 B049 8307 47DD 5484 B0A7 2FD2

To claim this, I am signing this object:

vikraman

;;; dart-init.el -- dart
;;; Commentary:

;;; Code:

(require 'auto-complete)
(require 'cl)

(defun dart--goto-line (line)
  (goto-char (point-min))

vikraman

import smoke._

import akka.actor._
import akka.routing.RoundRobinRouter
import akka.pattern.ask
import akka.util.Timeout
import scala.concurrent.duration._
import scala.concurrent.Await

object NotFoundException extends Exception("Not found")

vikraman

#
# Automatically generated file; DO NOT EDIT.
# Linux/x86 3.7.5-hardened-r1 Kernel Configuration
#
# CONFIG_64BIT is not set
CONFIG_X86_32=y
CONFIG_X86=y
CONFIG_INSTRUCTION_DECODER=y
CONFIG_OUTPUT_FORMAT="elf32-i386"
CONFIG_ARCH_DEFCONFIG="arch/x86/configs/i386_defconfig"

vikraman

<?xml version="1.0" encoding="UTF-8"?>
<interface>
  <requires lib="gtk+" version="2.24"/>
  <!-- interface-naming-policy project-wide -->
  <object class="GtkWindow" id="mainWindow">
    <property name="can_focus">False</property>
    <property name="title" translatable="yes">Greeter</property>
    <child>
      <object class="GtkVBox" id="vbox">
        <property name="visible">True</property>

vikraman

package com.example

import java.nio.ByteBuffer
import org.joda.time.DateTime
import com.thinkaurelius.titan.core.AttributeSerializer

class DateTimeSerializer extends AttributeSerializer[DateTime] {

  private val serialVersionUID = 272513079663L