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
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

#![feature(decl_macro)]

trait MemLayout where Self:Sized {
    // size, excluding trailing padding
    fn size() -> usize {
        core::mem::size_of::<Self>()
    }
    /// highest alignment among the members 
    /// of the product
    fn alignment() -> usize;

lovely-error

inductive NatNum : Type | zero | succ (n:NatNum)


def add (a b:NatNum): NatNum := 
  match a with | .zero => b | .succ n => .succ (add n b)


#eval (add (.succ (.succ .zero)) (.succ (.succ .zero)))

#check add.induct

lovely-error

homogenise the repr of generics / dyn Trait / (*mut/*const/&/&mut) dyn Trait
 
abstract value = (generic / dyn Trait / (*mut/*const/&/&mut) dyn Trait) value;
abstracted function = (takes at least one arg that is abstract or returns abstract value) and the fun is nonspecialisible;
at the 'lower level' abstract args are represented by wide pointers;
devise some opt passes to 'degeneralise' uses of abstracted funs at some sites;
specifically: 
1. uses within an 'inner world' (libs with visible impl)
2. cross bondry code must be generated to adhere to the wide pointer repr tho