Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

Specification.FOL

Description

This module provides the specification of first-order logic, i.e. its operators, rules and some examples. This module extends Specification.Prop

Synopsis

Documentation

Operators of first-order logic.

Each entry is a triple (alias, operator, arity), where alias is ASCII text the parser also accepts and the operator is usually a unicode symbol.

Operators are inherited from operatorsProp.

Infix predicates of first-order logic.

Each entry is a pair (alias, predicate), where alias is ASCII text the parser also accepts.

Quantifiers of first-order logic.

Each entry is a pair (alias, quantifier), where alias is ASCII text the parser also accepts and quantifier is a unicode symbol.

The standard Fitch-style natural deduction rules for first-order logic.

Extends rulesProp with rules for ∀, ∃ and =.

A list of example Proofs shown in the sidebar, each paired with a display name.

Arguments

:: URI	The current `URI` of the application.
-> Maybe Proof	An optional `Proof` decoded from the URL; falls back to the first example proof.
-> Maybe Bool	Initial state of onMobile
-> Bool	Possibly a previous sidebarToggle state.
-> Model

Constructs the initial Model for first-order-logic.