the theory of substitution is started ...

compare

work in progress

Restoring and fixing the old version

a development about pure lambda calculus

- additions in basic_2
- bugfix in BTM.html

- local environment refinement for the first recursive lemma on validity preservation
- focalized equivalence
- some corrections

match

match

compare con terminatore

match

some corrections

some words decapitalized :)

milestone table in foreword
--Questa linea, e quelle sotto essa, saranno ignorate--

M    index.html

match

milestone with end date of lambda_delta_1

compare

Match machine (multi)

progress

Parallel move machine.

Match machine (multi-tape)

Finished copy turing machine (multi-tape)

some more lemmata

copy machine (multi-tape) completed

- one axiom removed from sd
- traces added to auto to make it work
- bugfix in Makefile
- more notation and existentials for staff to be committed
- some minor additions

progress

progress

progress

progress
e

basic lemmas

addenda

inject.ma

while_multi.ma

- mac (ma count)
  small program to count the number of characters (not bytes) in a .ma
  file excluding (possibly nested) comments, repeated spaces, and escape
  characters in strings
- lambda_delta:
  Makefile updated to use mac

if_multi.ma

done

- commit completed!!
  The static type of <W>.T is now the static type of T.
  This allows to prove that each valid term has a static type as
expected!

New multi tapes machines

- commit of the component: static
- notation updates missing in former commit

- predefined_virtuals: nwe characters
- lib: some additions
- lambda_delta: commit of the components gramma, substitution, unfold
  - we parked the support for the "bt-reduction"
  - some renaming ...

- we set up the support for the "bt-reduction" of Automath literature
- we now use the STIX GENERAL fonts for a better rendering of U+2B43

an addition ...

- some additions and corrections

One useless Obj.magic removed.

- additions in basic_2
- substitution of downloadable logo is now complete!

- some confluence results for focalized reduction and computation
- more notation to be used later on ....

- milestone update in basic_2
- the new logo for the Crux is now linked to the site
- version update for xhtbl

context-free parallel reduction on closures is confluent!

- xhtbl: we added the construction + to place several keys in one cell
- basic_2_src: corrected and updated to use the operator +

updates in basic_2 ...

- parallel reduction for local environments: we proved the equivalence
between the old context-sensitive version and the focalized version
- as a result, the context-sensitive version disappears with its derivatives

Downgrades buggy destruct patch.

Removes debug prints that were left from last commit.

This patch allows generation of minimally dependent discrimination principles
for inductive types, in the case where Leibniz equality is used.

bugfix in Makefiles

- updates in basic_2

- full commit for the transtive closure of ltpss!

additions to basic_2

- partial commit (static component only)
- results on the transitive closure of ltpss

- some additions to basic_2
- new logo for lambda_delta

- partial commit (unfold component only)
  we introduced the transitive closure of ltpss,
  which we now use in the definition of thin

More work on inserting UnsafeCoerce in argument applications only when needed.

GHC.Prim.Any fixed

the partial commit continues ...

1. deriving (Show) no longer used because it fails on empty types
2. pretty-printing of types fixed: application arguments never had
   parentheses
3. Top replaced with GHC.Prim.Any

partial update in basic_2 ...

lambda_delta: partial commit ...

Composite coercions are now extracted too.

Name mangling until separate extraction is implemented.

Code to make all global names in a file fresh.

Capitalization of variables bound in patterns fixed.

...

Fixed indentation, which is semantic in Haskell.

(Part of previous two commits)

(Part of previous commit)

Extraction is now integrated with the usual machinery for serialization of
commands.

Top used also for fixes.

Match in types handled using top.

Match in types handled using Top.

Dead code removed.

Match in classification of non-terms taken in account.
We take the sup of the classification of all branches according to the
order

`Proposition < `PropKind < `Type < `Kind < `KindOrType

Known bug fixed: the rhs of a match over a small singleton inductive type
needed delifting to take it out its lhs.

progress in uni_step

Basics/logic.ma no longer raises exception.
Many workaround introduced to feed arguments to polymorphically kinded functions.

Bug fixed: when extracting pattern matching on singleton types it is possible
that a type is faced during the computation of the type of its constructor.
Ad-hoc patch added.

...

Fixed pretty-printing of types of variables bound in patterns.

Patterns are now computed according to the extracted constructor type.

pattern arguments where printed in reverse order

Bug fixed: rhs in match were printed in wrong context.

...

...

Code for computing patterns the way Haskell likes them (lhs + rhs).
Currently bugged:
 - some DeBrujin problems in the rhs
 - ignores the extracted type of the constructor (uses the CiC type)
 - does not perform eta-expansion when needed

Fixed pretty-printing of mutual recursive stuff and improved machinery to
pretty print references.

...

1. fixed pretty-printing of constructors, type variables, etc.
2. added UnsafeCoerce to pattern matching in an over-approximating way

Self contained now.

1. added Skip to terms to maintain consistency between Rels and context
   (required for pretty printing)

Fixed left/right context distinction in inductive types.

Pretty printing of context (variable refreshing) fixed.