lovely-error

import Mathlib
set_option pp.proofs true in
example
  {V:Real}{n1:Int}{r1 : (2:Real) = V}
  {eq1:@HEq { i:Int // n1 = i } ⟨n1, rfl⟩ { i:Int // V = ↑i } ⟨(2:Int), Eq.symm r1⟩ }
: n1 = 2 ∧ (HEq (rfl (a:=n1)) (Eq.symm r1))
:= by
  -- cases eq1
  admit

lovely-error

macro "rwi" pat:term "=>" new:term ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ])

macro "rwi" pat:term "=>" new:term "at" loc:Lean.Parser.Tactic.locationHyp ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ] at $loc)

lovely-error

import Mathlib
import Lean.Meta

macro "rwi" pat:term "=>" new:term ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ])

macro "rwi" pat:term "=>" new:term "at" loc:Lean.Parser.Tactic.locationHyp ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ] at $loc)

def wmap : Type _ -> Type _ -> Type _ | A, B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i

lovely-error

module REG (CLK, WE, D, O);

  parameter BITWIDTH = 1;
  parameter [BITWIDTH-1:0] INIT = '0;

  input CLK;
  input WE;
  input [BITWIDTH-1:0] D;
  output [BITWIDTH-1:0] O;

lovely-error

use core::marker::PhantomData;
use core::mem::ManuallyDrop;

#[repr(C)] #[derive(Copy, Clone)]
union TaggedPtr64Repr<T> {
    num: u64,
    tag: ManuallyDrop<T>,
}

lovely-error

import Mathlib

example (p1: (V:Rat) = I * R)(vnz: Not (V = 0))(rnz: Not (R = 0)) : R = (I *  R ^ 2) / V := by
  let target := p1
  let s1 : V = I * R <-> V / V = I * R / V := by 
    exact (iff_true_right (congrFun (congrArg HDiv.hDiv p1) V)).mpr p1
  rw [s1] at target
  let v_on_v_one: V / V = 1 := by
    exact (div_eq_one_iff_eq vnz).mpr rfl
  rw [v_on_v_one] at target

lovely-error

#![feature(decl_macro)]
macro d($ptr:expr) { unsafe { *$ptr } }
macro p($val:expr) { &raw mut $val }
macro pc($val:expr) { &raw const $val }

lovely-error

import Batteries


def NModB251CC8 := Vector (Fin 251) 4
def MAX_VAL := (250 * 251^0) + (250 * 251^1) + (250 * (251 ^ 2)) + (250 * (251 ^ 3))
def NModSC := Fin (MAX_VAL + 1)

def from_NModB251CC8_to_Nat : NModB251CC8 -> Nat | i => (i.zipWithIndex.map (fun ⟨ a , i ⟩ => a * ((251:Nat) ^ i))).foldl Nat.add 0

example : from_NModB251CC8_to_Nat (Vector.mk #[250,250,250,250] (by decide)) < MAX_VAL + 1 := by trivial

lovely-error

#include <stdio.h>
#include <stdbool.h>

void lmao (bool cond) {
  void* jmp_addr ;
  __asm__ goto volatile (
    "mov %[true_label], %[jmp_addr]\n\t"
    "mov %[false_label], %%rbx\n\t"
    "test %[cond], %[cond]\n\t"
    "cmovz %%rbx, %[jmp_addr]\n\t"

lovely-error

AMD

Internals [https://www.youtube.com/watch?v=KN_i-ay0y1A&list=PLB1fSi1mbw6IKbZSPz9a2r2DbnHWnLbF-&index=32] Dispatch [https://llvm.org/docs/AMDGPUUsage.html#kernel-dispatch] HSA API [https://rocm.docs.amd.com/projects/ROCR-Runtime/en/docs-6.2.4/api-reference/api.html] HSA SPEC [https://hsafoundation.com/wp-content/uploads/2021/02/HSA-SysArch-1.2.pdf] CLC [https://github.com/HSAFoundation/CLOC]

NVDA