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:
{-# OPTIONS --cubical #-} | |
module _ where | |
open import Cubical.Core.Everything | |
open import Cubical.Foundations.Everything | |
infixr 20 _∷_ | |
data M {ℓ} (A : Type ℓ) : Type ℓ where |
(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) |
(** * 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 := |
{-# 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 |
I hereby claim:
To claim this, I am signing this object:
;;; dart-init.el -- dart | |
;;; Commentary: | |
;;; Code: | |
(require 'auto-complete) | |
(require 'cl) | |
(defun dart--goto-line (line) | |
(goto-char (point-min)) |
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") |
# | |
# 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" |
<?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> |
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 |