alahijani

module Euclid

import Syntax.PreorderReasoning

%default total

Divides : (divisor, dividend : Nat) -> Type
Divides d n = (q : Nat ** (n = q * d))

data Direction = LTR | RTL

Rich-Harris

I've been deceiving you all. I had you believe that Svelte was a UI framework — unlike React and Vue etc, because it shifts work out of the client and into the compiler, but a framework nonetheless.

But that's not exactly accurate. In my defense, I didn't realise it myself until very recently. But with Svelte 3 around the corner, it's time to come clean about what Svelte really is.

Svelte is a language.

Specifically, Svelte is an attempt to answer a question that many people have asked, and a few have answered: what would it look like if we had a language for describing reactive user interfaces?

A few projects that have answered this question:

Rich-Harris

A modest proposal for a first-class destiny operator equivalent in Svelte components that's also valid JS.

Svelte 2 has a concept of computed properties, which are updated whenever their inputs change. They're powerful, if a little boilerplatey, but there's currently no place for them in Svelte 3.

This means that we have to use functions. Instead of this...

<!-- Svelte 2 -->
<h1>HELLO {NAME}!</h1>

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

-

System:    Host: godbog Kernel: 4.10.0-38-generic x86_64 (64 bit gcc: 5.4.0)
           Desktop: Cinnamon 3.6.7 (Gtk 3.18.9-1ubuntu3.3) dm: lightdm Distro: Linux Mint 18.3 Sylvia
Machine:   Mobo: Micro-Star model: Z370-A PRO (MS-7B48) v: 1.0
           Bios: American Megatrends v: 2.10 date: 09/05/2017
CPU:       Hexa core Intel Core i7-8700K (-HT-MCP-) cache: 12288 KB
           flags: (lm nx sse sse2 sse3 sse4_1 sse4_2 ssse3 vmx) bmips: 44352
           clock speeds: min/max: 800/4700 MHz 1: 899 MHz 2: 900 MHz 3: 899 MHz 4: 900 MHz 5: 899 MHz
           6: 899 MHz 7: 899 MHz 8: 958 MHz 9: 899 MHz 10: 900 MHz 11: 930 MHz 12: 966 MHz
Graphics:  Card: NVIDIA Device 1b80 bus-ID: 01:00.0 chip-ID: 10de:1b80
           Display Server: X.Org 1.18.4 drivers: nvidia (unloaded: fbdev,vesa,nouveau)

kmassada

Libvirt

yum group install -y "Development Tools"
yum -y install qemu-kvm libvirt virt-install bridge-utils libvirt-devel  libxslt-devel libxml2-devel libvirt-devel libguestfs-tools-c

echo "net.ipv4.ip_forward = 1"|sudo tee /etc/sysctl.d/99-ipforward.conf
sysctl -p /etc/sysctl.d/99-ipforward.conf

ms-tg

/**
 * ```
 * Does JDK8's Optional class satisfy the Monad laws?
 * =================================================
 *   1.  Left identity:  true
 *   2.  Right identity: true
 *   3.  Associativity:  true
 *
 * Yes, it does. 
 * ```

syl20bnr

#!/usr/bin/env python
#
# author: syl20bnr (2013)
# goal: Focus the nth window in the current workspace (limited to 10 firsts)
#
# Example of usage in i3 config:
#
# bindsym $mod+0   exec focus_win.py -n 0
# bindsym $mod+1   exec focus_win.py -n 1
# ...              ...

risavkarna

SET SCHEMA CHALLENGE3;

DROP TYPE UNKNOWN_TWEET_T;
CREATE TYPE UNKNOWN_TWEET_T AS TABLE 
(	
  "ID" BIGINT NOT NULL,							-- Unique identifier for this Tweet
  "TEXT" nvarchar(800) NOT NULL,            	-- The actual text of the status update
  "TRUNCATED" TINYINT NOT NULL default 0,  		-- (1 = True, 0 = False) Indicates whether the text was truncated, for example, as a result of a retweet exceeding the 140 character Tweet length. Truncated text will end in ellipsis, like this ... 
  "SOURCE" nvarchar(255),                   	-- Utility used to post the Tweet, as an HTML-formatted string. (e.g. 'web')
  "CREATED_AT" DATETIME not null,				-- UTC time when this Tweet was created.