meditans

Hai questo problema, diciamo che test/shell.nix sia:

{ pkgs ? import <nixpkgs> {} }:
with pkgs; mkShell { buildInputs = [ pkgs.hello ]; }

tu fai:

> cd test

test> hello

juanjovazquez

object labelled {
  opaque type Field[K <: String, +V] = V
  object Field {
    def apply[K <: String, V](v: V): Field[K, V] = v

    extension on [K <: String, V](field: Field[K, V]) {
      def value: V = field
    }
  }

AndrasKovacs

open import Data.Unit
open import Data.Product

infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_

data Obj : Set where
  ∙    : Obj
  base : Obj
  _*_  : Obj → Obj → Obj

AndrasKovacs

{-# OPTIONS --postfix-projections --without-K --safe #-}

{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.

Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:

nrinaudo

Introduction

I was recently asked to explain why I felt disappointed by Haskell, as a language. And, well. Crucified for crucified, I might as well criticise Haskell publicly.

First though, I need to make it explicit that I claim no particular skill with the language - I will in fact vehemently (and convincingly!) argue that I'm a terrible Haskell programmer. And what I'm about to explain is not meant as The Truth, but my current understanding, potentially flawed, incomplete, or flat out incorrect. I welcome any attempt at proving me wrong, because when I dislike something that so many clever people worship, it's usually because I missed an important detail.

Another important point is that this is not meant to convey the idea that Haskell is a bad language. I do feel, however, that the vocal, and sometimes aggressive, reverence in which it's held might lead people to have unreasonable expectations. It certainly was my case, and the reason I'm writing this.

Type classes

I love the concept of type class

wilbowma

#lang racket/base

(require
 (for-syntax
  racket/base
  syntax/parse)
 (rename-in
  racket/base
  [#%datum old-datum]
  [set! old-set!]))

VictorTaelin

Typ
: {T : (Typ T)} Type
= [T] {self : (T self)} Type

Rat
: (Typ Rat)
= [self]
  {-Prop : {self : (Rat self)} {fold : (Prop self fold)} Type}
  {succ  : !succ {-pred : (Rat pred)} {fold : (Prop pred fold)} (Prop (Rat.succ pred) (succ -pred fold))}
  {zero  : !zero (Prop Rat.zero zero)}

gallais

module scope where

import Level as L
open import Data.Nat.Base
open import Data.Vec hiding (_>>=_)
open import Data.Fin.Base
open import Data.String
open import Data.Maybe as Maybe
open import Data.Product as Prod
open import Relation.Nullary

FradSer

The latest beta (3.5) includes separate color settings for light & dark mode. Toggling dark mode automatically switches colors.

Vist iTerm2 homepage or use brew install iterm2-beta to download the beta. Thanks @stefanwascoding.

---

1. Add switch_automatic.py to ~/Library/ApplicationSupport/iTerm2/Scripts/AutoLaunch with:

Blaisorblade

{-# OPTIONS --type-in-type --no-positivity-check  #-}

module InconsistentImpredicativeSums where
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Product
open import Data.Empty
-- hiding (⊥-elim)
-- open import Data.Empty.Irrelevant