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.  <[email protected]>

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

srghma

structure WithIsChangedOrWillBeUpdated (α : Type) where
  v : α
  isChanged : Bool
  willBeUpdated : Bool

def withIsChangedOrWillBeUpdated [BEq a] (before now editing : a) : WithIsChangedOrWillBeUpdated a :=
  { v := now,
    isChanged := not (now == before),
    willBeUpdated := not (now == editing) }

srghma

import Std.Data.HashMap

open Std

structure DiffResult2 (s r a : Type) where
  same    : HashMap String s
  removed : HashMap String r
  added   : HashMap String a

def diffListsBy (befores : HashMap String r) (nows : HashMap String a) : DiffResult2 a r a :=