Cogent
334
An Introduction to
Cogent
Getting the
Cogent
Compiler
A First Program
The Business End:
add
add
, version 1: Hello, Cogent!
add
, version 2: Let’s Consider…
add
, version 3: An Iffy Question
add
, version 4: A New Type of Trouble
add
, version 5: Tag! You’re It
add
, version 6: Polymorphism
add
, version 7: But In General…
add
, version 8: A Pattern Emerges
Gum, Glue, and Antiquoted C
A more complicated example: a Fibonacci iterator
Abstract Types and Polymorphic Functions
Example: polymorphic abstract types
Building Isabelle Proofs
Cogent
Reference Manual
Surface Syntax
Lexical Syntax
Comments
Identifiers
Literals
Core Syntax
Types
Type Basics
Primitive Types
Composite Types
Type Definitions
Restricted Types
Linear Types
Boxed and Unboxed Types
Partial Record Types
Readonly Types
Working with Values
Patterns
Simple Patterns
Composite Patterns
Expressions
Terms
Basic Expressions
General Expressions
Expression Usage Rules
Using Values of Linear Types
Using Values of Readonly Types
Programs
Including Files
Toplevel Definitions
Value Definitions
Function Definitions
Abstract Definitions
Polymorphic Definitions
Antiquoted C
Antiquotes
$id
: Introducing Identifiers
$ty
: Talking Types
$exp
: Embedding Expressions
$spec
: Specifying Casts
$esc
and
$escstm
: No Escape In Sight
Antiquoted C
Cheatsheet
Overview
Modes in the compiler
Function definitions
Type declarations / Typedef’s
Escape sequences
Expressions
Using the
Cogent
Compiler
Commands
All Flags
Installation Guide
In a Nutshell
Detailed Instructions
Dependencies
Install
Cogent
dependencies
Install
Cogent
Test your installation
Common Issues and Troubleshooting
Cabal Version
Missing Dependencies
Could not resolve dependency
isa-parser
Verification
Dependencies
Generated Theory Files
Building/Running The Generated Files
In Jedit
On the command line
Examples
A Simple Example
A More Involved Example
Common Errors
ACInstall
Appendices
Bibliography
Colophon
About Cogent
About This Documentation
Contributors
Documentation Todo
Cogent
Docs
»
Appendices
»
Bibliography
Edit on GitHub
Next
Previous
Bibliography
¶
Todo
(jashankj, 2020-02-13): add some references.