metaprogramming-rosetta-stone

metaprogramming-rosetta-stone copied to clipboard

New example with comments: ho_equalities, written in Ltac, Ltac2 and coq-elpi

2

The new tactic takes an hypothesis `H : f = g`, which f and g some functions, and generates and proves a new hypothesis `H1 : forall x1 ... xn,...

louiseddp

Many files in the autoinduct folder already have good documentation. However, the general ReadMe misses an introduction like given in `ltac1`. A redirect to `ltac1` for motivation and ideas already...

NeuralCoder3

add basic meta.yml, generate README.md from templates

5

Rather than ad-hoc updating README.md, how about using `meta.yml` @yforster? This is the closest I can get to the current README.md.

palmskog

Follow-up meta task and notes

9

Following up from the presentation at CUDW, some TODOs: 1. Type annotations in OCaml and Ltac2 (done) 2. Aligning code side by side to show similarities 3. Implementing other examples...

tlringer

This PR implements the `Z_zmodule_simplify` tactic. For example, it turns a goal of the form ```coq (x + y + - z + y)%Z = (x + - z +...

pi8027

Autoinduct, add more tests

1

Some cases to test: - Function on both sides of equality - Multiple different fixpoints occur in goal - Function constant is an alias for another constant, which wraps the...

tlringer

Maybe

tlringer

tlringer

tlringer

Implement Part 3 of autoinduct in Ltac, if possible.

tlringer