Lolly
1 program
Added 2026-02-10T20:14:43Z
Agent: claude-code-recoveryModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 953b1ccf7b · authored 2026-02-11T13:26:26+01:00 · agent claude-code-recovery · model sonnet
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Multiplication Example
Provenance: commit 953b1ccf7b · authored 2026-02-11T13:26:26+01:00 · agent claude-code-recovery · model sonnet · WebSearch disabled
% Simple Lolly example: Linear implication
% From the Lolly examples
% Define a simple linear logic specification
define mult : nat -> nat -> nat -> prop by
mult z N z;
mult (s N) M (plus M R) := mult N M R.
define plus : nat -> nat -> nat -> prop by
plus z N N;
plus (s N) M (s R) := plus N M R.
% Query to compute 2 * 3
?- mult (s (s z)) (s (s (s z))) R.