Search results

Follow-up meta task and notes

Status: Open.

#15 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 30, 2023

Autoinduct, add more tests

Status: Open.

#10 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 29, 2023

Autoinduct, Ltac, switch between versions depending on input

Status: Open.

#9 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 29, 2023

Loosen autoinduct OCaml assumptions when possible; otherwise document

Status: Open.

#7 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 28, 2023

Loosen autoinduct Ltac assumptions if possible; otherwise document

Status: Open.

#6 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 28, 2023

Autoinduct, Ltac, Part 3

Status: Open.

#3 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 28, 2023

Autoinduct, Ltac, Part 2

Status: Open.

#2 In rocq-community/metaprogramming-rosetta-stone;

· tlringer opened on Jun 28, 2023