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) = 5Each line has a prescribed number of morae; the numbers of morae go 5, 7, 5.
∧ morae (p 2) = 7
∧ morae (p 3) = 5.
where
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.
User.
Document.
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.
where
nobody ⇒ User.
has-perm? u:User, d:Document ⇒ Bool.
Quick Start
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
Install dependencies:
jpm --local deps
Build Pantagruel:
jpm --local build
Move the pant application to your PATH:
mv build/pant ~/bin
Learn More
