add a type class for stepindices

parameterize the definition of ofes

monoids

algebra big_op and list

camera

naming

updates

local updates

gset

proofmode classes

gmap

add finite step-index file with instantiation

more algebras

cofe solver

algebras

instance precedence

more algebras

more algebras

more algebras

small fixes

turn dist_later into a record

make step-index a canonical structure and a type class

primitive projections for step-index

add instances to fix left ids

cleanup + document missing left_ids

add less-or-equal to step-index interface

base logic files

turn dist_later into a record

make step-index a canonical structure and a type class

enable primitive projections more often

add less-or-equal to step-index interface

enable primitive projections more often

si prop

misc

turn dist_later into a record

make step-index a canonical structure and a type class

primitive projections for step-index

add less-or-equal to step-index interface

more algebras

fixes

si prop

misc

turn dist_later into a record

make step-index a canonical structure and a type class

primitive projections for step-index

add less-or-equal to step-index interface

formatting

re-add comment that got gobbled up while merging; formatting

hopefully fix ci

fix name

names

fix name mangling

add FIXME

add comments to the step index file

typos

comments

Apply 1 suggestion(s) to 1 file(s)

unset primitive projections for uPred

minimize changes to existing proof script

nits

minimize changes

remove later_or for now

regression

regression

regression

Comments and formatting

lbcompl

tweak

links to papers

comment on the addition of ile

explain more about the canonical structure + type class hack