pedrominicz

import group_theory.quotient_group
import set_theory.ordinal

-- https://math.stackexchange.com/a/370073/783124

namespace cardinal

open quotient_group

variables {α : Type*} [group α] {s : set α} [is_subgroup s]

sflicht

import linear_algebra.basic 
       linear_algebra.direct_sum_module 
       linear_algebra.basis 
       linear_algebra.finsupp_vector_space
       ring_theory.noetherian
       data.finsupp
       tactic


open_locale classical

fpvandoorn

import tactic -- all

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

geo2a

Tactic Notation
  "`Begin " constr(lhs) := idtac.

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) :=
  (stepl lhs by proof).

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) "`End" :=
  (now stepl lhs by proof).

hashbrowncipher

#!/bin/bash
# Depends on zstd (>1.3.6) and aws-cli
set -o errexit
set -o nounset
set -o pipefail

# Set kernel.core_pattern = | coredump_uploader.sh %P %s %E
PID=$1
shift
SIGNAL=$1

kbuzzard

/-
Copyright (c) 2018 Kevin Buzzard and Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Buzzard, Patrick Massot.

This file is to a certain extent based on `quotient_module.lean` by Johannes Hölzl.

Quotient groups
===============

edmundsmith

Method for Emulating Higher-Kinded Types in Rust

Intro

I've been fiddling about with an idea lately, looking at how higher-kinded types can be represented in such a way that we can reason with them in Rust here and now, without having to wait a couple years for what would be a significant change to the language and compiler.

There have been multiple discussions on introducing higher-ranked polymorphism into Rust, using Haskell-style Higher-Kinded Types (HKTs) or Scala-looking Generalised Associated Types (GATs). The benefit of higher-ranked polymorphism is to allow higher-level, richer abstractions and pattern expression than just the rank-1 polymorphism we have today.

As an example, currently we can express this type:

kbuzzard

import algebra.group
import linear_algebra.tensor_product
import tactic.ring

universe u

section canonical

variables {R : Type u} [comm_ring R] {m n : ℕ} (h : m = n)
  {A : ℕ → Type u} [∀ n, add_comm_group (A n)] [∀ n, module R (A n)]

HadrienG2

Hello, Rust community!

My name is Hadrien and I am a software performance engineer in a particle physics lab. My daily job is to figure out ways to make scientific software use hardware more efficiently without sacrificing its correctness, primarily by adapting old-ish codebases to the changes that occured in the software and computing landscape since the days where they were designed:

• CPU clock rates and instruction-level parallelism stopped going up, so optimizing code is now more important.
• Multi-core CPUs went from an exotic niche to a cheap commodity, so parallelism is not optional anymore.
• Core counts grow faster than RAM prices go down, so multi-processing is not enough anymore.
• SIMD vectors become wider and wider, so vectorization is not a gimmick anymore.

steveklabnik

use std::env;
use std::io;
use std::io::prelude::*;
use std::fs::File;

#[derive(Debug)]
enum Error {
    Io(io::Error),
    Program(&'static str),
}