Plaster
New
List
Login
text
apl
aspx
asterisk
brainfuck
c
c++hdr
c++src
cassandra
ceylon
clojure
clojurescript
cmake
cobol
coffeescript
common-lisp
crystal
csharp
css
cypher-query
cython
d
dart
diff
django
dockerfile
dylan
ebnf
ecl
ecmascript
edn
eiffel
ejs
elm
erb
erlang
ez80
factor
fcl
feature
forth
fortran
fragment
gfm
go
gql
groovy
gss
haml
handlebars-template
haskell
haxe
hive
html
http
httpd-php
httpd-php-open
hxml
ini
java
javascript
json
jsp
jsx
julia
kotlin
latex
less
literate-haskell
lua
mariadb
markdown
mbox
mirc
mscgen
msgenny
mssql
mumps
mysql
n-triples
nesc
nginx-conf
nsis
objectivec
octave
oz
pascal
perl
pgp
pgp-keys
pgp-signature
pgsql
php
pig
plsql
properties
protobuf
puppet
python
q
rpm-changes
rpm-spec
rsrc
ruby
rustsrc
sas
sass
scala
scheme
scss
sieve
slim
smarty
solr
soy
sparql-query
spreadsheet
sql
squirrel
stex
styl
swift
systemverilog
tcl
textile
tiddlywiki
tiki
tlv
tornado
ttcn-asn
ttcn-cfg
turtle
twig
typescript
typescript-jsx
vb
vbscript
velocity
verilog
vertex
vhdl
vue
webidl
xml
xml-dtd
xquery
xu
yaml
z80
default
Visibility:
public
unlisted
private
(defmacro define-symbolic-types (&rest names) (let ((types (make-hash-table))) (dotimes (n (1+ (length names))) (alexandria:map-combinations (lambda (combination) (let ((name (gensym))) (dolist (c combination) (push name (gethash c types '()))))) names :length n)) `(progn ,@(loop for name in names for symbols = (gethash name types) collect `(deftype ,name () '(member ,@symbols))) (values-list ',names)))) (defun true? (p) "Is P the universal set, i.e. is our statement P true?" (values (subtypep 't p))) (deftype implies (p q) "Are all elements of P elements of Q? (This is basically SUBTYPEP again.)" `(or (not ,p) ,q)) (deftype equals (p q) `(and (implies ,p ,q) (implies ,q ,p))) (define-symbolic-types a b c) (print (true? '(implies a a))) (print (true? '(implies a b))) (print (true? '(implies (and a (implies a b)) b))) (print (true? '(equals (and a b) (not (or (not a) (not b))))))