screwlisp

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481398/homespun-acl2-handler-bind-condition-handling

#acl2 simple introduction to acl2 for the #commonLisp inclined.

loop$, apply$, thms oh my.

In particular, I implement a model of a simple case of the common lisp condition system that is directly compatible with both ansi common lisp and acl2. (a computational logic for applicative common lisp).

#firstOrderLogic #theoremProving #programming #logic #example

Technically this is in support of my lisp / moo compatibility layer but I am not going to beleaguer the tag.

Homespun acl2 handler-bind condition handling - lispmoo2 by screwtape

Even though LambdaMOO’s MOO language is not obsessed with first order logic, in my common lisp condition system mooing I am obsessed with first order logic. To that end I have here initially impleme...

itch.io
Apr 6 at 5:32amWeb
Show threadscrewlisp19h ago

Addendum Summarizing / lining up the #commonLisp #conditionSystem version with the #acl2 #logic version:

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481671/summary-how-common-lisp-conditions-line-up-to-the-acl2-theorem-accidental-common-lisp-metaobject-protocol-eg

Also an unintended #mop #demo

Summary how common lisp conditions line up to the acl2 theorem + accidental common lisp metaobject protocol e.g. - lispmoo2 by screwtape

We should do the ansi common lisp side of the acl2 first order logic condition theorem. (define-condition awkward () ((keys :initarg :keys :reader keys))) Quick fix: mop the keys to be the ones your c...

itch.io