Library Combi.LRrule.extract: Extracting the implementation to OCaml

A certified OCaml implementation

We extract to OCaml the implementation of the Robinson-Schensted correspondance and The Littlewood-Richardson Rule.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import mpoly.
Require Import subseq partition ordtype Schensted congr plactic Greene Greene_inv
        std stdtab skewtab therule implem.

Require Import Wf_nat.
Extraction Inline Wf_nat.lt_wf_rec1 Wf_nat.lt_wf_rec
  Wf_nat.lt_wf_ind Wf_nat.gt_wf_rec Wf_nat.gt_wf_ind.

Extract Inductive bool => "bool" [ "true" "false" ].

Extract Inductive list => "list" [ "[]" "(::)" ].

Extract Inductive prod => "(*)" [ "(,)" ].


Definition disp := Order.NatOrder.nat_display.
Definition RS := (@RS disp nat).
Definition RSbijnat := (@RSbij disp nat).
Definition RSbijinvnat := (@RSbijinv disp nat).
Definition RStabnat := (@RStab disp nat).
Definition RStabinvnat := (@RStabinv disp nat).


The Littlewood-Richardson Rule

Extraction "src/LRrule/lrcoeff.ml"
           LRcoeff LRyamtab_list
.