use INF and SUP on conditionally complete lattices in multivariate analysis

add SUP and INF for conditionally complete lattices

use bdd_above and bdd_below for conditionally complete lattices

generalize SUP and INF to the syntactic type classes Sup and Inf

added some N2M caching

also generalize fixed types

generalize types when synthetizing n2m (co)recursors, to facilitate reuse

nicer error message in case of duplicates

use int example like in the rest of IMP (instead of nat)

dropped dead code

fact generalization and name consolidation

streamlined setup of linear arithmetic

make 'try0' return faster when invoked as part of 'try'

careful with lists of different lengths

split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')

better error handling

more robust treatment of dead variables in n2m

more robust n2m w.r.t. 'let's

tuning

strengthened tactic

made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)

handle constructor syntax in n2m primcorec

typo

made sugared 'coinduct' theorem construction n2m-proof

moved code around

tuning

make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)

conceal definition

more exercises

more exercises