leodemoura

theorem CategoryTheory.Linear.smul_comp.{w, v₁, u₁} : ∀ {R : Type w} [inst : Semiring R] {C : Type u₁}
  [inst_1 : CategoryTheory.Category C] [inst_2 : @CategoryTheory.Preadditive C inst_1]
  [self : @CategoryTheory.Linear R inst C inst_1 inst_2] (X Y Z : C) (r : R)
  (f :
    @Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Y)
  (g :
    @Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) Y Z),
  @Eq
    (@Quiver.Hom C (@CategoryTheory.CategoryStruct.toQuiver C (@CategoryTheory.Category.toCategoryStruct C inst_1)) X Z)
    (@CategoryTheory.CategoryStruct.comp C (@CategoryTheory.Category.toCategoryStruct C inst_1) X Y Z

leodemoura

import Lean

-- The `elab` command is used to define new commands, tactics, and term syntax.
-- We are using it here to define a `#reformat <term>` command that elaborates
-- the given term and then pretty prints it.
open Lean Meta Elab Command Term in
elab "#reformat " s:term : command => liftTermElabM do
  -- `elabTerm` converts `s : Syntax` into an expression `e` without using an expected type (i.e., `none`)
  -- `withSynthesize x` forces pending elaboration problems in `x` to be executed, it applies default instances too.
  let e ← withSynthesize do elabTerm s none

leodemoura

leomoura@bcd074b16892 lean4 % ps aux | grep lean
leomoura          4379  23.7  6.8 473465344 2288928   ??  Us    3:16PM  26:10.71 /Users/leomoura/.elan/toolchains/leanprover--lean4---nightly-2024-06-26/bin/lean --worker file:///Users/leomoura/projects/LNSym/Arm/MemoryProofs.lean
leomoura          8645   8.0  4.2 419422032 1424720   ??  Us    3:35PM   4:02.30 /Users/leomoura/projects/lean4/build/release/stage1/bin/lean --worker file:///Users/leomoura/projects/lean4/build/release/ome.lean
leomoura          6446   5.8  1.8 445861872 598112   ??  Us    3:25PM  14:30.48 /Users/leomoura/projects/lean4/build/release/stage1/bin/lean --worker file:///Users/leomoura/projects/lean4/build/release/bvdecide.lean
leomoura         17438   0.0  0.2 412706864  81424   ??  Ss    4:56PM   0:06.18 /Users/leomoura/projects/lean4/build/release/stage0/bin/lean --worker file:///Users/leomoura/projects/lean4/src/Lean/Elab/MutualDef.lean
leomoura         11167   0.0  0.0 412277792   2368   ??  Ss    3:48PM   0:00.51 /Users/leomoura/pro

leodemoura

test 2057
    Start 2057: leanlaketest_init

2057: Test command: /bin/bash "-c" "
               set -eu
               export PATH=/Users/leomoura/projects/lean4/build/release/stage1/bin:$PATH LEAN_CC=/usr/bin/clang CXX='/usr/bin/clang++  -O3 -DNDEBUG' LEANC_OPTS=' -O3 -DNDEBUG'
               LAKE=lake ./test.sh"
2057: Working Directory: /Users/leomoura/projects/lean4/src/lake/tests/init
2057: Test timeout computed to be: 1500
2057: + ./clean.sh

leodemoura

def strict : Bool -> Type
| true => Unit
| false => Empty

def f : (n:Nat) -> strict (n > 0) -> Nat := by
  intros n
  match n with
  | .zero => simp; exact fun i => by nomatch i
  | n@(.succ _) => simp; exact fun () => n

leodemoura

import Lean

opaque g (n : Nat) : Nat

@[simp] def f (i n m : Nat) :=
  if i < n then
    f (i+1) n (g m)
  else
    m
termination_by n - i

leodemoura

import Std.Data.HashMap

open Std

/-
In Lean, a hash map has type

def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
  ...

leodemoura

/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import init.core init.data.nat.basic
open Decidable List

universes u v w

leodemoura

static object * map1(object * l) {
    if (obj_tag(l) == 0) {
        return l;
    } else {
        object * h     = cnstr_obj(l, 0);
        object * t     = cnstr_obj(l, 1);
        object * new_h = box(unbox(h) + 1);
        object * new_t = map1(t);
        object * r     = alloc_cnstr(1, 2, 0);

leodemoura

import system.io 

universes u v w r 

/-- 
   Asymmetric coroutines `coroutine α δ β` takes inputs of type `α`, yields elements of type `δ`,
   and produces an element of type `β`. 

   Asymmetric coroutines are so called because they involve two types of control transfer operations:
   one for resuming/invoking a coroutine and one for suspending it, the latter returning