srghma

 ✘  ~/projects/mm0   learn ±✚  ./examples/test_pub_theorem.sh
=== Setting up test files ===
=== First Verification (Base case) ===
elab test_thm.mm1
elabbed test_thm.mm1
1 sorts, 1 term/def, 3 ax/thm
Verification succeeded!
=== Experiment 1: Adding a new PUB theorem not declared in MM0 ===
elab test_thm.mm1
elabbed test_thm.mm1

srghma

// ==UserScript==
// @name         Djinni Quick Apply Pro
// @namespace    http://tampermonkey.net/
// @version      2.2.0
// @description  Automate job applications on Djinni.co directly via Tampermonkey
// @author       You
// @match        https://djinni.co/*
// @grant        none
// ==/UserScript==

srghma

-- config
def colorize := false

def cyan (s : String) := if colorize then s!"\x1b[36m{s}\x1b[0m" else s
def yellow (s : String) := if colorize then s!"\x1b[33m{s}\x1b[0m" else s
def green (s : String) := if colorize then s!"\x1b[32m{s}\x1b[0m" else s
def red (s : String) := if colorize then s!"\x1b[31m{s}\x1b[0m" else s


-- 1. Helper to find integer powers of 2 (returns e ≥ 0)

srghma

Notebook[{Cell[
BoxData[RowBox[{}]],"Input",CellLabel -> "In[5]:= ",ExpressionUUID -> "a5eda00a-dbbb-408b-ae55-06412828302d"],Cell[
CellGroupData[
{Cell[
BoxData[RowBox[{RowBox[{"Manipulate","[",RowBox[{RowBox[{"Plot3D","[",RowBox[
{RowBox[{"{",RowBox[{RowBox[{RowBox[{"x","^","2"}]," ","+"," ",RowBox[{"y","^","2"}]}],","," ",RowBox[
{RowBox[{"-",RowBox[{"x","^","2"}]}]," ","-"," ",RowBox[{"y","^","2"}]}]}],"}"}],","," ",RowBox[
{"{",RowBox[{"x",","," ",RowBox[{"-","2"}],","," ","2"}],"}"}],","," ",RowBox[{"{",RowBox[
{"y",","," ",RowBox[{"-","2"}],","," ","2"}],"}"}],","," ","\n"," ",RowBox[{"RegionFunction"," ","\[Rule]"," ",RowBox[
{"Function","[",RowBox[{RowBox[{"{",RowBox[{"x",","," ","y",","," ","z"}],"}"}],","," ",RowBox[

srghma

-- 1. The raw data structure
inductive BinderImplementation (e : Type) where
  | Op : BinderImplementation e → Array (BinderImplementation e) → BinderImplementation e

-- 2. The validation predicate
def BinderImplementation.isWF {e : Type} : BinderImplementation e → Prop
  | .Op what whatElse => 
      what.isWF ∧ whatElse.size > 0 ∧ (∀ x ∈ whatElse, x.isWF)

-- 3. The actual Type

srghma

 ~/projects/mm0/mm0-hs   master  for i in ../examples/*.mm[01]; do                  
  ./.stack-work/dist/x86_64-linux-nix/ghc-9.10.3/build/mm0-hs/mm0-hs compile "$i" \
    && echo "=================== OK ==================== $i" \
    || echo "=================== ERR =================== $i"
done
depth limit exceeded
=================== ERR =================== ../examples/assembler-new.mm1
../examples/assembler-old.mm1:7:24:
  |
7 | local def _x00: char = 0;

srghma

import Lean

open Lean Elab Command Meta

-- Macro to create a structure by omitting specified fields
syntax "elab_omit" ident "[" term,* "]" : term

-- Macro to create a structure by picking specified fields  
syntax "elab_pick" ident "[" term,* "]" : term

srghma

sudo virsh net-start default sudo EDITOR=nvim virsh dumpxml win11-2 > /tmp/win11-2.xml sudo EDITOR=nvim virsh edit win11-2

srghma

// node find-dbfield-without-model.js
const path = require('path')
const { Project, SyntaxKind } = require('ts-morph')

const project = new Project({
  tsConfigFilePath: '/home/srghma/jss/api/tsconfig.json',
})

project.addSourceFilesAtPaths('/home/srghma/jss/api/src/models/db/**/*.ts')

srghma

Copyright (c) Serhii Khoma.  <srghma@gmail.com>

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in