Skip to content

Instantly share code, notes, and snippets.

@mcdoll
mcdoll / test.lean
Last active January 31, 2024 09:21
Classes heavy decorated sets
import Mathlib.Algebra.Group.Defs
import Mathlib.Data.SetLike.Basic
namespace Zulip
section Inter
class Inter (S1 S2 S3 : Type*) (M : outParam (Type*)) [SetLike S1 M] [SetLike S2 M] [SetLike S3 M] where
inter : S1 → S2 → S3
inter_coe (s1 : S1) (s2 : S2) : (inter s1 s2 : Set M) = (s1 : Set M) ∩ s2
@mcdoll
mcdoll / gist:22365c871885f6b31ed2f24cbd85c3e0
Created January 4, 2020 01:04
atomic_cxchg_acq crashing on arm
{
"arch": "arm",
"data-layout": "e-m:e-p:32:32-Fi8-i64:64-v128:64:128-a:0:32-n32-S64",
"env": "",
"executables": true,
"features": "+strict-align,+v7,+a8",
"linker-flavor": "ld.lld",
"linker": "rust-lld",
"llvm-target": "arm-none-eabi",
"max-atomic-width": 64,