Library zoo.prelude

Library zoo.tactics

Library zoo.options

Library zoo.ltac2.Array

Library zoo.ltac2.Constr

Library zoo.ltac2.Constructor

Library zoo.ltac2.Control

Library zoo.ltac2.Debug

Library zoo.ltac2.Env

Library zoo.ltac2.Ident

Library zoo.ltac2.Ind

Library zoo.ltac2.List

Library zoo.ltac2.Message

Library zoo.ltac2.Notations

Library zoo.ltac2.Option

Library zoo.ltac2.Std

Library zoo.ltac2.String

Library zoo.common.function

Library zoo.common.countable

Library zoo.common.relations

Library zoo.common.math

Library zoo.common.option

Library zoo.common.list

Library zoo.common.listne

Library zoo.common.binder

Library zoo.common.fin_maps

Library zoo.common.gset

Library zoo.common.gmultiset

Library zoo.common.treemap

Library zoo.common.string

Library zoo.common.format

Library zoo.common.typeclasses

Library zoo.iris.algebra.base

Library zoo.iris.algebra.big_op

Library zoo.iris.algebra.view

Library zoo.iris.algebra.auth

Library zoo.iris.algebra.mono

Library zoo.iris.algebra.monopo

Library zoo.iris.algebra.monopoi

Library zoo.iris.algebra.lib.auth_option

Library zoo.iris.algebra.lib.twins

Library zoo.iris.algebra.lib.auth_mono

Library zoo.iris.algebra.lib.auth_monoi

Library zoo.iris.proofmode.tokens

Library zoo.iris.proofmode.sel_patterns

Library zoo.iris.proofmode.intro_patterns

Library zoo.iris.proofmode.coq_tactics

• Starting and stopping the proof mode
• Basic rules
• False
• Pure
• Intuitionistic
• Implication and wand
• Conjunction splitting
• Separating conjunction splitting
• Combining
• Conjunction/separating conjunction elimination
• Framing
• Disjunction
• Forall
• Existential
• Modalities
• Accumulate hypotheses
• Invariants
• Rewriting
• Löb
• Introduction of modalities

Library zoo.iris.proofmode.ltac_tactics

• Misc
• Start a proof
• Generate a fresh identifier
• Context manipulation
• Assumptions
• False
• Making hypotheses intuitionistic or pure
• Basic introduction tactics
• Revert
• The specialize and pose proof tactics
• The apply tactic
• Disjunction
• Conjunction and separating conjunction
• Existential
• Modality introduction
• Later
• Update modality
• Basic destruct tactic
• Combinining hypotheses
• Introduction tactic
• Destruct and PoseProof tactics
• Induction
• Löb Induction
• Assert
• Rewrite
• Update modality
• Invariant

Library zoo.iris.proofmode.proofmode

Library zoo.iris.diaframe.base

Library zoo.iris.diaframe.tactics

Library zoo.iris.diaframe.diaframe

Library zoo.iris.bi.big_op.base

Library zoo.iris.bi.big_op.big_sepL

Library zoo.iris.bi.big_op.big_sepL2

Library zoo.iris.bi.big_op.big_sepL_seq

Library zoo.iris.bi.big_op.big_sepL_seqZ

Library zoo.iris.bi.big_op.big_sepL3

Library zoo.iris.bi.big_op.big_sepM

Library zoo.iris.bi.big_op.big_sepS

Library zoo.iris.bi.big_op.big_sepMS

Library zoo.iris.bi.big_op.big_op

Library zoo.iris.bi.lib.atomic

• Now the coq-level tactics

Library zoo.iris.base_logic.algebra.twins

Library zoo.iris.base_logic.lib.base

Library zoo.iris.base_logic.lib.agree

Library zoo.iris.base_logic.lib.saved_pred

Library zoo.iris.base_logic.lib.saved_prop

Library zoo.iris.base_logic.lib.excl

Library zoo.iris.base_logic.lib.ghost_var

Library zoo.iris.base_logic.lib.ghost_pred

Library zoo.iris.base_logic.lib.ghost_prop

Library zoo.iris.base_logic.lib.ghost_list

Library zoo.iris.base_logic.lib.oneshot

Library zoo.iris.base_logic.lib.twins

Library zoo.iris.base_logic.lib.auth_dgset

Library zoo.iris.base_logic.lib.auth_frac

Library zoo.iris.base_logic.lib.auth_gmultiset

Library zoo.iris.base_logic.lib.auth_mono

Library zoo.iris.base_logic.lib.auth_monoi

Library zoo.iris.base_logic.lib.auth_nat_max

Library zoo.iris.base_logic.lib.auth_nat_min

Library zoo.iris.base_logic.lib.auth_twins

Library zoo.iris.base_logic.lib.semiauth_twins

Library zoo.iris.base_logic.lib.mono_list

Library zoo.iris.base_logic.lib.mono_gmap

Library zoo.iris.base_logic.lib.mono_gset

Library zoo.iris.base_logic.lib.mono_gmultiset

Library zoo.iris.base_logic.lib.prophet_map

Library zoo.iris.base_logic.lib.spsc_prop

Library zoo.iris.base_logic.lib.subpreds

Library zoo.iris.base_logic.lib.subprops

Library zoo.iris.base_logic.lib.fupd

Library zoo.iris.base_logic.lib.cinv

Library zoo.language.location

Library zoo.language.syntax

Library zoo.language.metatheory

Library zoo.language.physical_equality

Library zoo.language.state

Library zoo.language.semantics

Library zoo.language.language

Library zoo.language.notations

Library zoo.language.tactics

Library zoo.language.typeclasses

Library zoo.program_logic.state_interp

Library zoo.program_logic.bwp

Library zoo.program_logic.bwp_adequacy

Library zoo.program_logic.wp

Library zoo.program_logic.wp_adequacy

Library zoo.program_logic.atomic

Library zoo.program_logic.itype

Library zoo.program_logic.prophet_typed

Library zoo.program_logic.prophet_bool

Library zoo.program_logic.prophet_nat

Library zoo.program_logic.prophet_identifier

Library zoo.program_logic.prophet_wise

Library zoo.program_logic.prophet_multi

Library zoo.program_logic.identifier

Library zoo.program_logic.structural_equality

Library zoo.program_logic.counter

Library zoo.program_logic.biglater

Library zoo.proofmode

Library zoo.diaframe.symb_exec.defs

Library zoo.diaframe.symb_exec.wp

Library zoo.diaframe.hints

Library zoo.diaframe.specs

Library zoo.diaframe.diaframe

Library zoo_std.base

Library zoo_std.diverge

Library zoo_std.assert

Library zoo_std.assume

Library zoo_std.for_

Library zoo_std.ref_

Library zoo_std.option

Library zoo_std.goption__types

Library zoo_std.goption__code

Library zoo_std.goption__opaque

Library zoo_std.goption

Library zoo_std.int__types

Library zoo_std.int__code

Library zoo_std.int__opaque

Library zoo_std.int

Library zoo_std.optional__types

Library zoo_std.optional__code

Library zoo_std.optional__opaque

Library zoo_std.optional

Library zoo_std.goptional__types

Library zoo_std.goptional__code

Library zoo_std.goptional__opaque

Library zoo_std.goptional

Library zoo_std.list__types

Library zoo_std.list__code

Library zoo_std.list__opaque

Library zoo_std.list

Library zoo_std.clist__types

Library zoo_std.clist__code

Library zoo_std.clist__opaque

Library zoo_std.clist

Library zoo_std.glist__types

Library zoo_std.glist__code

Library zoo_std.glist__opaque

Library zoo_std.glist

Library zoo_std.chain__types

Library zoo_std.chain__code

Library zoo_std.chain__opaque

Library zoo_std.chain

Library zoo_std.xchain__types

Library zoo_std.xchain__code

Library zoo_std.xchain__opaque

Library zoo_std.xchain

Library zoo_std.xtchain__types

Library zoo_std.xtchain__code

Library zoo_std.xtchain__opaque

Library zoo_std.xtchain

Library zoo_std.xdlchain__types

Library zoo_std.xdlchain__code

Library zoo_std.xdlchain__opaque

Library zoo_std.xdlchain

Library zoo_std.xtdlchain__types

Library zoo_std.xtdlchain__code

Library zoo_std.xtdlchain__opaque

Library zoo_std.xtdlchain

Library zoo_std.chunk

Library zoo_std.array__types

Library zoo_std.array__code

Library zoo_std.array__opaque

Library zoo_std.array

Library zoo_std.atomic_array__types

Library zoo_std.atomic_array__code

Library zoo_std.atomic_array

Library zoo_std.dynarray_1__types

Library zoo_std.dynarray_1__code

Library zoo_std.dynarray_1__opaque

Library zoo_std.dynarray_1

Library zoo_std.dynarray_2__types

Library zoo_std.dynarray_2__code

Library zoo_std.dynarray_2__opaque

Library zoo_std.dynarray_2

Library zoo_std.inf_array__types

Library zoo_std.inf_array__code

Library zoo_std.inf_array__opaque

Library zoo_std.inf_array

Library zoo_std.bqueue__types

Library zoo_std.bqueue__code

Library zoo_std.bqueue__opaque

Library zoo_std.bqueue

Library zoo_std.queue_1__types

Library zoo_std.queue_1__code

Library zoo_std.queue_1__opaque

Library zoo_std.queue_1

Library zoo_std.queue_2__types

Library zoo_std.queue_2__code

Library zoo_std.queue_2__opaque

Library zoo_std.queue_2

Library zoo_std.queue_3__types

Library zoo_std.queue_3__code

Library zoo_std.queue_3__opaque

Library zoo_std.queue_3

Library zoo_std.stack__types

Library zoo_std.stack__code

Library zoo_std.stack__opaque

Library zoo_std.stack

Library zoo_std.xdeque__types

Library zoo_std.xdeque__code

Library zoo_std.xdeque__opaque

Library zoo_std.xdeque

Library zoo_std.deque__types

Library zoo_std.deque__code

Library zoo_std.deque__opaque

Library zoo_std.deque

Library zoo_std.domain__types

Library zoo_std.domain__code

Library zoo_std.domain

Library zoo_std.mutex__types

Library zoo_std.mutex__code

Library zoo_std.mutex__opaque

Library zoo_std.mutex

Library zoo_std.condition__types

Library zoo_std.condition__code

Library zoo_std.condition__opaque

Library zoo_std.condition

Library zoo_std.semaphore__types

Library zoo_std.semaphore__code

Library zoo_std.semaphore__opaque

Library zoo_std.semaphore

Library zoo_std.mpsc_flag__types

Library zoo_std.mpsc_flag__code

Library zoo_std.mpsc_flag__opaque

Library zoo_std.mpsc_flag

Library zoo_std.spsc_waiter__types

Library zoo_std.spsc_waiter__code

Library zoo_std.spsc_waiter__opaque

Library zoo_std.spsc_waiter

Library zoo_std.mpsc_waiter__types

Library zoo_std.mpsc_waiter__code

Library zoo_std.mpsc_waiter__opaque

Library zoo_std.mpsc_waiter

Library zoo_std.ivar_1__types

Library zoo_std.ivar_1__code

Library zoo_std.ivar_1__opaque

Library zoo_std.ivar_1

Library zoo_std.ivar_2__types

Library zoo_std.ivar_2__code

Library zoo_std.ivar_2__opaque

Library zoo_std.ivar_2

Library zoo_std.ivar_3__types

Library zoo_std.ivar_3__code

Library zoo_std.ivar_3__opaque

Library zoo_std.ivar_3

Library zoo_std.ivar_4__types

Library zoo_std.ivar_4__code

Library zoo_std.ivar_4__opaque

Library zoo_std.ivar_4

Library zoo_std.mvar__types

Library zoo_std.mvar__code

Library zoo_std.mvar__opaque

Library zoo_std.mvar

Library zoo_std.lazy__types

Library zoo_std.lazy__code

Library zoo_std.lazy__opaque

Library zoo_std.lazy

Library zoo_std.random__types

Library zoo_std.random__code

Library zoo_std.random__opaque

Library zoo_std.random

Library zoo_std.random_state__types

Library zoo_std.random_state__code

Library zoo_std.random_state__opaque

Library zoo_std.random_state

Library zoo_std.random_round__types

Library zoo_std.random_round__code

Library zoo_std.random_round__opaque

Library zoo_std.random_round

Library zoo_persistent.base

Library zoo_persistent.pstack__types

Library zoo_persistent.pstack__code

Library zoo_persistent.pstack__opaque

Library zoo_persistent.pstack

Library zoo_persistent.pqueue__types

Library zoo_persistent.pqueue__code

Library zoo_persistent.pqueue__opaque

Library zoo_persistent.pqueue

Library zoo_persistent.parray_1__types

Library zoo_persistent.parray_1__code

Library zoo_persistent.parray_1__opaque

Library zoo_persistent.parray_1

Library zoo_persistent.parray_2__types

Library zoo_persistent.parray_2__code

Library zoo_persistent.parray_2__opaque

Library zoo_persistent.parray_2

Library zoo_persistent.pstore_1__types

Library zoo_persistent.pstore_1__code

Library zoo_persistent.pstore_1__opaque

Library zoo_persistent.pstore_1

Library zoo_persistent.pstore_2__types

Library zoo_persistent.pstore_2__code

Library zoo_persistent.pstore_2__opaque

Library zoo_persistent.pstore_2

Library zoo_persistent.puf__types

Library zoo_persistent.puf__code

Library zoo_persistent.puf__opaque

Library zoo_persistent.puf

Library zoo_saturn.base

Library zoo_saturn.mpmc_stack_1__types

Library zoo_saturn.mpmc_stack_1__code

Library zoo_saturn.mpmc_stack_1__opaque

Library zoo_saturn.mpmc_stack_1

Library zoo_saturn.mpmc_stack_2__types

Library zoo_saturn.mpmc_stack_2__code

Library zoo_saturn.mpmc_stack_2__opaque

Library zoo_saturn.mpmc_stack_2

Library zoo_saturn.mpmc_bstack__types

Library zoo_saturn.mpmc_bstack__code

Library zoo_saturn.mpmc_bstack__opaque

Library zoo_saturn.mpmc_bstack

Library zoo_saturn.inf_mpmc_queue_1__types

Library zoo_saturn.inf_mpmc_queue_1__code

Library zoo_saturn.inf_mpmc_queue_1__opaque

Library zoo_saturn.inf_mpmc_queue_1

Library zoo_saturn.inf_mpmc_queue_2__types

Library zoo_saturn.inf_mpmc_queue_2__code

Library zoo_saturn.inf_mpmc_queue_2__opaque

Library zoo_saturn.inf_mpmc_queue_2

Library zoo_saturn.mpmc_tqueue_2__types

Library zoo_saturn.mpmc_tqueue_2__code

Library zoo_saturn.mpmc_tqueue_2__opaque

Library zoo_saturn.mpmc_tqueue_2

Library zoo_saturn.spsc_bqueue__types

Library zoo_saturn.spsc_bqueue__code

Library zoo_saturn.spsc_bqueue__opaque

Library zoo_saturn.spsc_bqueue

Library zoo_saturn.mpmc_bqueue__types

Library zoo_saturn.mpmc_bqueue__code

Library zoo_saturn.mpmc_bqueue__opaque

Library zoo_saturn.mpmc_bqueue

Library zoo_saturn.spmc_queue__types

Library zoo_saturn.spmc_queue__code

Library zoo_saturn.spmc_queue__opaque

Library zoo_saturn.spmc_queue

Library zoo_saturn.mpsc_queue_1__types

Library zoo_saturn.mpsc_queue_1__code

Library zoo_saturn.mpsc_queue_1__opaque

Library zoo_saturn.mpsc_queue_1

Library zoo_saturn.mpsc_queue_2__types

Library zoo_saturn.mpsc_queue_2__code

Library zoo_saturn.mpsc_queue_2__opaque

Library zoo_saturn.mpsc_queue_2

Library zoo_saturn.mpsc_queue_3__types

Library zoo_saturn.mpsc_queue_3__code

Library zoo_saturn.mpsc_queue_3__opaque

Library zoo_saturn.mpsc_queue_3

Library zoo_saturn.mpmc_queue_1__types

Library zoo_saturn.mpmc_queue_1__code

Library zoo_saturn.mpmc_queue_1__opaque

Library zoo_saturn.mpmc_queue_1

Library zoo_saturn.mpmc_queue_2__types

Library zoo_saturn.mpmc_queue_2__code

Library zoo_saturn.mpmc_queue_2__opaque

Library zoo_saturn.mpmc_queue_2

Library zoo_saturn.bag_1__types

Library zoo_saturn.bag_1__code

Library zoo_saturn.bag_1__opaque

Library zoo_saturn.bag_1

Library zoo_saturn.bag_2__types

Library zoo_saturn.bag_2__code

Library zoo_saturn.bag_2__opaque

Library zoo_saturn.bag_2

Library zoo_saturn.inf_ws_deque_1__types

Library zoo_saturn.inf_ws_deque_1__code

Library zoo_saturn.inf_ws_deque_1__opaque

Library zoo_saturn.inf_ws_deque_1

Library zoo_saturn.inf_ws_deque_2__types

Library zoo_saturn.inf_ws_deque_2__code

Library zoo_saturn.inf_ws_deque_2__opaque

Library zoo_saturn.inf_ws_deque_2

Library zoo_saturn.ws_bdeque_1__types

Library zoo_saturn.ws_bdeque_1__code

Library zoo_saturn.ws_bdeque_1__opaque

Library zoo_saturn.ws_bdeque_1

Library zoo_saturn.ws_bdeque_2__types

Library zoo_saturn.ws_bdeque_2__code

Library zoo_saturn.ws_bdeque_2__opaque

Library zoo_saturn.ws_bdeque_2

Library zoo_saturn.ws_deque_1__types

Library zoo_saturn.ws_deque_1__code

Library zoo_saturn.ws_deque_1__opaque

Library zoo_saturn.ws_deque_1

Library zoo_saturn.ws_deque_2__types

Library zoo_saturn.ws_deque_2__code

Library zoo_saturn.ws_deque_2__opaque

Library zoo_saturn.ws_deque_2

Library zoo_parabs.base

Library zoo_parabs.ws_deques_public__types

Library zoo_parabs.ws_deques_public__code

Library zoo_parabs.ws_deques_public__opaque

Library zoo_parabs.ws_deques_public

Library zoo_parabs.ws_deques_private__types

Library zoo_parabs.ws_deques_private__code

Library zoo_parabs.ws_deques_private__opaque

Library zoo_parabs.ws_deques_private

Library zoo_parabs.waiter__types

Library zoo_parabs.waiter__code

Library zoo_parabs.waiter__opaque

Library zoo_parabs.waiter

Library zoo_parabs.waiters__types

Library zoo_parabs.waiters__code

Library zoo_parabs.waiters__opaque

Library zoo_parabs.waiters

Library zoo_parabs.ws_hub_fifo__types

Library zoo_parabs.ws_hub_fifo__code

Library zoo_parabs.ws_hub_fifo__opaque

Library zoo_parabs.ws_hub_fifo

Library zoo_parabs.ws_hub_std__types

Library zoo_parabs.ws_hub_std__code

Library zoo_parabs.ws_hub_std__opaque

Library zoo_parabs.ws_hub_std

Library zoo_parabs.pool__types

Library zoo_parabs.pool__code

Library zoo_parabs.pool__opaque

Library zoo_parabs.pool

Library zoo_parabs.future__types

Library zoo_parabs.future__code

Library zoo_parabs.future__opaque

Library zoo_parabs.future

Library zoo_parabs.algo__types

Library zoo_parabs.algo__code

Library zoo_parabs.algo__opaque

Library zoo_parabs.algo

Library zoo_parabs.vertex__types

Library zoo_parabs.vertex__code

Library zoo_parabs.vertex__opaque

Library zoo_parabs.vertex

Library examples.fibonacci

Library examples.pool_counter__types

Library examples.pool_counter__code

Library examples.pool_counter__opaque

Library examples.pool_counter

Library examples.pool_quicksort__types

Library examples.pool_quicksort__code

Library examples.pool_quicksort__opaque

Library examples.pool_quicksort

Library examples.future_fibonacci__types

Library examples.future_fibonacci__code

Library examples.future_fibonacci__opaque

Library examples.future_fibonacci

Library examples.vertex_fibonacci__types

Library examples.vertex_fibonacci__code

Library examples.vertex_fibonacci__opaque

Library examples.vertex_fibonacci

Library examples.vertex_simple__types

Library examples.vertex_simple__code

Library examples.vertex_simple__opaque

Library examples.vertex_simple

Library unix.unix

Library zoo_eio.base

Library zoo_eio.rcfd__types

Library zoo_eio.rcfd__code

Library zoo_eio.rcfd__opaque

Library zoo_eio.rcfd

Library zoo_boxroot.base

Library zoo_boxroot.gc

Library zoo_boxroot.boxroot

Library zoo_kcas.kcas_1__types

Library zoo_kcas.kcas_1__code

Library zoo_kcas.kcas_1__opaque

Library zoo_kcas.kcas_1

Library zoo_kcas.kcas_2__types

Library zoo_kcas.kcas_2__code

Library zoo_kcas.kcas_2__opaque

Library zoo_kcas.kcas_2

Library zoo_partition.partition__types

Library zoo_partition.partition__code

Library zoo_partition.partition__opaque

Library zoo_partition.partition