Serhii Khoma srghma

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

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

	~/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;

	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

	// 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')

	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

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

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