TOTBWF

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []

aaronmdjones

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

My resignation from freenode staff
==================================

I joined the freenode staff in March 2019 [1].

Before I joined the staff, Freenode Ltd was sold [2] to a person named
Andrew Lee as part of a sponsorship deal. The informal terms of that

laughinghan

• any: magic, ill-behaved type that acts like a combination of never (the proper [bottom type]) and unknown (the proper [top type])
  • Anything except never is assignable to any, and any is assignable to anything at all.
  • Identities: any & AnyTypeExpression = any, any | AnyTypeExpression = any
  • Key TypeScript feature that allows for [gradual typing].
• unknown: proper, well-behaved [top type]
  • Anything at all is assignable to unknown. unknown is only assignable to itself (unknown) and any.
  • Identities: unknown & AnyTypeExpression = AnyTypeExpression, unknown | AnyTypeExpression = unknown

• Prefer over any whenever possible. Anywhere in well-typed code you're tempted to use any, you probably want unknown.

konn

{-# LANGUAGE ConstraintKinds, DataKinds, DeriveGeneric, DerivingVia    #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances   #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds, ScopedTypeVariables, StandaloneDeriving        #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators #-}
{-# LANGUAGE UndecidableInstances                                      #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Aeson.Generic.DerivingVia
     ( StrFun(..), Setting(..), SumEncoding'(..), DefaultOptions, WithOptions(..)
     , -- Utility type synonyms to save ticks (') before promoted data constructors

parsonsmatt

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}

gmalecha

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
module ShapeIndexed where
import Data.Constraint

mietek

module DataCodata where

open import Data.Product using (_×_ ; _,_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)


--------------------------------------------------------------------------------


case : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}

playground.rs

#![feature(unboxed_closures)] 
#![feature(fn_traits)]

#[derive(Clone)]
struct Pr {
    pat: i32 //, mat: Matcher<'a,'a>
}

type MState = i32;

kbauer

SetTitleMatchMode RegEx
#IfWinActive .*Comic Rocket webcomic list - Google Chrome

ComicRocketChangePage(bynum)
{
  oldclip := clipboard
  Send ^l
  Sleep 50
  Send ^c
  Sleep 50

talwai

 { echo -ne "HTTP/1.0 200 OK\r\nContent-Length: $(wc -c <some.file)\r\n\r\n"; cat some.file; } | nc -l 8080