Poem = [Line].
Line = String.
scans? p: Poem ⇒ Bool.
scans? p → #p = 3.
A haiku is a poem of exactly three lines.
scans? p → morae (p 1) = 5
Each line has a prescribed number of morae; the numbers of morae go 5, 7, 5.
∧ morae (p 2) = 7
∧ morae (p 3) = 5.
morae l: Line ⇒ Nat.
A mora is like a syllable, but shorter; it is known in Japanese as 音. To evaluate a line we count its morae.
Pantagruel is a computer program designed to help human beings think and communicate rigorously.
The human thinker can write a description of some system of rules, propositions, or behaviours in Pantagruel’s syntax and the Pantagruel document checker will attempt to validate the description.
Pantagruel constrains the human thinker into some of the syntactic forms of first-order logic and computer programming. In doing so it is hoped that the thinker will encounter elements of their thought which require further precision.
Through some simple constraints on the introduction and use of terms, Pantagruel might be able to assist the thinker in eliminating certain kinds of ambiguity to which natural language is prone.
owner d : Document ⇒ User.
check-out u:User, d:Document.
A specification for a small document management system.
owner d = nobody ∧ has-perm? u d → owner d′ = u.
A user may check out a document if they have permission to access it and it’s not currently checked out.
owner d ≠ nobody ∨ ¬(has-perm? u d) → owner d′ = owner d.
nobody ⇒ User.
has-perm? u:User, d:Document ⇒ Bool.
Install Pantagruel from AUR
yay -S pantagruel
Install Pantagruel from Source (requires the Janet language and package manager)
Clone the Pantagruel repository:
git clone https://github.com/subsetpark/pantagruel.git
jpm --local deps
jpm --local build
pant application to your
mv build/pant ~/bin