Squirrel
Introduction
Reference manual
Notations
Lexical conventions
Infix operators
Logic
Types
Base types
Type variables and polymorphism
General types
Binders and tags
Terms
Terms with binders
Multi-terms
Diff-terms
Macros
Formulas
Local formulas
Global formulas
Declarations
Terms
Names
Abstract functions
Operators
Built-ins
Cryptographic functions
Processes
Channels
Memory cells
Processes
Systems and actions
System-defined macros
System expressions
System contexts
Axioms and Lemmas
Proofs
Judgements
Logical variables
Hypotheses
Local judgement
Global judgement
Generalities
Tactic arguments
Intro patterns
Proof terms
Proof-term resolution
Reduction
Automatic simplification tactics
Tactics
Common errors
Tactics
Generic tactics
Common tactics
Local tactics
Global tactics
Structural tactics
Common tactics
Local tactics
Global tactics
Cryptographic tactics
Occurrence formula
Common tactics
Local tactics
Global tactics
Utility tactics
Commands
Tutorial
Protocol modelling
Messages
Basic assumption
Cryptographic assumptions
Protocols
Reachability properties
Macros
Formulas
Equivalence properties
Appendix
Indexes
Glossary index
Declaration index
Command index
Tactic index
Errors and warnings index
Index
Documenting Squirrel with Sphinx
TODO list generation
Squirrel objects
Notations
Objects
Squirrel directives
Squirrel roles
Common mistakes
Improper nesting
Overusing
:token:
Omitting annotations
Using the
..
squirreltop::
directive for syntax highlighting
Overusing plain quotes
Overusing the
example
directive
Tips and tricks
Nested lemmas
Abbreviations and macros
Advanced uses of notations
Bibliography
Squirrel
Index
Edit on GitHub
Index
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
L
|
M
|
N
|
O
|
P
|
Q
|
R
|
S
|
T
|
U
|
X
A
Abort (command)
abstract (declaration)
admit (tactic)
aenc (declaration)
apply (tactic)
,
[1]
Argument of cs should match a boolean (error)
assert (tactic)
assumption (tactic)
Assumption not over valid system (error)
auto (tactic)
autosimpl (tactic)
B
by (tactic)
byequiv (equiv tactic)
C
case (tactic)
case_study (equiv tactic)
cca1 (equiv tactic)
cdh (trace tactic)
channel (declaration)
clear (tactic)
collision (trace tactic)
congruence (trace tactic)
const (trace tactic)
constraints (tactic)
constseq (equiv tactic)
D
ddh (equiv tactic)
deduce (equiv tactic)
dependent induction (tactic)
depends (tactic)
destruct (tactic)
Did not find any conditional to analyze (error)
diffeq (equiv tactic)
E
enckp (equiv tactic)
enrich (equiv tactic)
eqnames (trace tactic)
eqtrace (trace tactic)
euf (trace tactic)
executable (trace tactic)
exists (tactic)
expand (tactic)
expandall (tactic)
F
fa (tactic)
fresh (tactic)
G
gdh (trace tactic)
generalize (tactic)
generalize dependent (tactic)
global (declaration)
H
hash (declaration)
have (tactic)
,
[1]
help (tactic)
hint rewrite (command)
I
id (tactic)
include (command)
induction (tactic)
intctxt (trace tactic)
intro (tactic)
L
left (tactic)
lemma (declaration)
lemmas (tactic)
localize (tactic)
M
max nested rewriting reached (error)
memseq (equiv tactic)
mutable (declaration)
N
name (declaration)
Nonrecursive Elimination Schemes (flag)
nosimpl (tactic)
Not dependent (error)
nothing to rewrite (error)
O
op (declaration)
Out of range position (error)
P
prf (equiv tactic)
print (command)
process (declaration)
prof (command)
project (trace tactic)
Proof (command)
Proof is not complete (error)
Q
Qed (command)
R
reduce (tactic)
refl (equiv tactic)
remember (tactic)
repeat (tactic)
Reset (command)
revert (tactic)
rewrite (tactic)
rewrite_equiv (trace tactic)
right (tactic)
rule bad systems (error)
S
search (command)
senc (declaration)
set (command)
show (tactic)
signature (declaration)
simpl (tactic)
smt (trace tactic)
split (tactic)
splitseq (equiv tactic)
subst (trace tactic)
sym (equiv tactic)
system (declaration)
T
trans (equiv tactic)
true (trace tactic)
try (tactic)
type (declaration)
U
undo (command)
Unequal arguments (error)
use (tactic)
X
xor (equiv tactic)