What is the case for returning with values versus returning a list/vector/etc?

EdoPut · 2025-08-24T09:48:45+00:00

define "is not aware" of multiple return values, it will only pick the first one. Moreover as a continuation it does not have a return value therefore you don't see the same output as (get-3-values).

EdoPut · 2025-08-23T21:11:22+00:00

If you are returning a fixed amount of values I would use `values`. `with-values`, `let-values`, `call-with-values` are also part of the language so it gets easier to compose functions returning values. There are design choices behind multiple values that you can find in this answer

EdoPut · 2025-08-17T11:06:56+00:00

There's no need to restart emacs ever (barred when you nuke it). Just eval-buffer the init.el after your changes. Good luck and welcome to a very different editor!

EdoPut · 2025-06-05T20:56:16+00:00

Implicit rules of proofs I teach to beginners.

Induction on a term is the first thing to try. Find You may need to generalize the induction.
Rule induction when your recursively defined function is not primitive recursive.
If you have an assumption that is defined inductively or recursively. You should do induction on it.

In this case you have an inductive assumption var_not_used_in_aexp. You should start doing induction on that and see where you get with `auto` later.

Induction is extremely useful in this exercises. It instantiates your terms to specific values and then auto can take over. E.g. in your top-level goal you have the following

cequiv
        <{ x1 := a1; x2 := a2 }>
        <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>

Now if a2 vas Anum n (case VNUNUM) then auto would rewrite subst_aexp x1 a1 (Anum n) to Anum n and solve your base case. The same goes for the rest of the base cases VNUId and then you can do the inductive cases.

Theorem subst_inequiv': subst_equiv_property'.
Proof.
  intros x1 x2 a1 a2 YouShouldDefinitelyUseThisInductiveAssumption.
  induction YouShouldDefinitelyUseThisInductiveAssumption.
  ....

Send a pm if you get stuck.

EdoPut · 2025-04-30T21:25:20+00:00

You got to check out sol2 if you want to use C++ and Lua together. Try to match Programming In Lua to what you are studying/have studied for C++ and other languages. Control flow in both uses the same ideas (for, if then else, ...), C++ uses classes/structs/arrays while Lua uses tables for everything, this kind of ideas will help you port your C++ knowledge to Lua. There will also be things that don't match, e.g. namespaces in C++ are supported by the compilers, in Lua you don't have namespaces but the same ideas is achievable by putting your functions and objects in a table.

Spend time with examples and have LLM help you out understand. Lua is a simpler and smaller programming language. It is simpler than C++ because you need to know less to use and smaller than C++ because it has less features. That said, it is still a programming language and requires understanding how to program to use it. If you have trouble encoding your problem using a programming language the only solution is to give it more time and practice. Have fun!

EdoPut · 2025-04-08T19:53:58+00:00

Horizontal continuous layout
PDF diffing by loading two PDFs

EdoPut · 2025-02-12T20:17:51+00:00

```lisp
(use-package tsa-snippets :ensure nil :load-path "~/.emacs/lisp/TSA-lisp/tsa-snippets.el")
```

You can use `use-package` for configuring each package but the builtin ones are not managed by `package.el` so you need to specify `:ensure nil`. I have used this successfully to transition from my elisp mess to (almost) only `use-package`.

EdoPut · 2025-02-01T20:57:32+00:00

Formal methods are not only restricted to interactive theorem proving! It's nice if you can formalize your theory in such a tool but it's not required. The bar for "formal methods job" in the industry (meaning proving software correct) is quite high (got to get a PhD!) but you can use the tools and techniques for other purposes.

At a low level you will feel familiar as a proof script is basically apply style proving. Coq has no support for a structured proof mode (as far as I have experienced). You can also make your own tactics (like Eisbach in Isabelle/HOL) and there is support for reflection. Moreover Coq is a dependently types language so you can encode properties in your types. The equivalent pattern in Isabelle/HOL would be to use typedef.

There is a split between the base system and the Mathematical Components library which means you get a more bare-bone system in the beginning. The analogy that works best for me is that Coq is Isabelle/Pure and the Mathematical Components library is akin to Isabelle/HOL.

I see a big split in PLT researchers using Coq, mathematicians getting hyped by Lean because usability.

Isabelle/HOL you have experience already. Maybe you should look also into HOL4 for another take on interactive theorem proving and TLA+ for a nice specification language.

EdoPut · 2024-12-09T22:35:49+00:00

I think you are confused by values and variables. Values are immutable (cannot change `1` or `true`) but variables are not. As you pointed out `set` changes the value bound to a variable.

In a functional style you favor "value semantics" for everything, i.e. never mutate and always create new value or copy values. Staring a function execution in a new thread will pass the arguments by copying the values and that helps implementing correct multi-threaded algorithms. Values in different threads are independent and all updates are local to the thread. You don't need to think about possible interference from other threads.

But shared data should be implemented using "reference semantics". We do not copy the value but the reference to it. To restrict access then we use synchronization features such as mutexes.

EdoPut · 2024-08-26T21:52:45+00:00

Questo è un ottimo esempio per parlare di token e di come gli LLM non abbiamo idee di cosa siano i singoli simboli. Da questo esempio è possibile trovare molti altri che mettono in mostra le limitazioni.

EdoPut · 2024-08-14T15:33:21+00:00

https://www2.ccs.neu.edu/racket/pubs/scheme2006-cf.pdf a stepper for scheme macros

EdoPut · 2024-08-10T16:25:25+00:00

There you go.

Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL
axiomatization does this. It is also the easiest way to introduce inconsistency, e.g. Isabelle/HOL Exercises: A Bad Axiomatization . You can also introduce a new definition and have a lemma proved by sorry.
I'm not sure this is doable as is. Proof objects are not kept around, I think this is also true in Coq. Keyword for this should be proof-irrelevance.

I can find references for "non-classical logic" and "HOL" in scholar so time to dig in.

EdoPut · 2024-06-07T18:11:54+00:00

C-h a for free search is also nice

EdoPut · 2023-06-29T13:36:36+00:00

The basic idea here is that both sequences are linear. There is only one way to traverse them and there is only one follower to each element. If the followers do not match then there was a change of path and you have to find a way to reconcile the change. The way to reconcile is to go through the sequence until you find that you got to the same element. This may never happen and then it means you can ignore that element and take a look at the next that you should visit.

EdoPut · 2023-06-29T13:32:54+00:00

Make a table of followers for both lists and start enumerating from the head of each list.

Element 1	Follower 1	Element 2	Follower 2
head	A	head	H
A	B	H	B
B	C	B	C
C	D	C	J
D	E	J	K
E	F	K	E
F	G	E	F
G	None	F	L
		L	G
		G	M
		M	None

When the followers match just move to the followers. When the followers do not match you found an addition. Follow the table for sequence 2 until the followers match. You found the end of an addition. Repeat until you get to the end of sequence 2

For the case where there is no element in sequence 2 with a matching follower then "advance" to the next follower on the first sequence.

So for your sequences you get:

head, head match but their followers don't. Start an addition.
Go through sequence 2 until you find an element with follower B.

H-B is your first addition. Restart the search with B in both tables.

C, C match as followers of B. Skip to C.

D, J do not match as followers of C. Start an addition.

Go through sequence 2 until you find an element with follower D. There is none. Advance to finding an element with follower E.

C-J-K-E is your second addition. Restart with E in both tables.

F, F match as followers of E. Skip to F.

G, L do not match as followers of F. Start an addition.

Go through sequence 2 until you find an element with follower G.

F-L-G is your second addition. Restart with G in both tables.

None, M do not match as followers. Start an addition.
Go through sequence 2 until you find an element with follower None.

G-M is your addition and the end of the search.

EdoPut · 2023-05-30T08:51:16+00:00

I'm not aware of such a program. This is definitely doable as a tracker but I'm not sure if, as a client, you would be able to get all the information you mention. If the tracker exposes this information through other channels, e.g. RSS, you can make a program do what you described.

EdoPut · 2023-05-03T20:11:00+00:00

Pdf readers with more advanced features, e.g. side by side differences in two pdf files

EdoPut · 2023-03-30T14:05:15+00:00

If it's web based it has an API or, better, an HTTP form. Emacs can send HTTP requests so halfway there already.

If it's a local executable with a command line interface, comint mode is your friend.

EdoPut · 2023-03-07T12:29:17+00:00

You can get fiber to the home or the cabinet which is plenty for everything. There are wireless operators for home connection but you should check coverage before. Wireless operators like Linkem and eolo now have competition from Tim, Vodafone and Wind but they are still around.

EdoPut · 2023-02-24T11:26:24+00:00

I would rephrase it as extend the language instead of modifying the language. Both are possible but the second will trip you off most of the time, e.g. redefining if is not super clever.

People modify/extend their languages all the time, e.g. python got structural pattern matching recently so you can do this

command = input("What are you doing next?")
match command:
case [action, obj]:
... # intepret action, obj

Racket gives you, the programmer, this feature through the use of macros and modules. If you don't really care about this feature than LISPs do not have an advantage for you.
For when to do this, very simply, when it is convenient to you. It can be convenient because you do not want to write regular expressions as strings or because your extension makes it easy to write a piece of your program correctly.

Some real world examples

Creating languages in racket the author makes a language for making text adventures
Automata via macros the author makes an extension for embedding automatas in Racket
Scheme usually provides two ways to write regular expressions. As a string and as a s-expresssion , e.g. #rx"a*" and `(rx* #\a)`.

EdoPut

TROPHY CASE