Finfun (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Finfun)

type __ = Obj.t

type 'rT finfun_on =

| Coq_finfun_nil
| Coq_finfun_cons of Fintype.Finite.sort * Fintype.Finite.sort list * 'rT * 'rT finfun_on

val finfun_rec : 
  Fintype.Finite.coq_type ->
  (Fintype.Finite.sort -> 'a1) ->
  Fintype.Finite.sort list ->
  'a1 finfun_on

val fun_of_fin_rec : 
  Fintype.Finite.coq_type ->
  Eqtype.Equality.sort ->
  Fintype.Finite.sort list ->
  'a1 finfun_on ->
  'a1

type 'rT finfun_of = 'rT finfun_on

val fun_of_fin : 
  Fintype.Finite.coq_type ->
  'a1 finfun_of ->
  Eqtype.Equality.sort ->
  'a1

module type Coq_finfun_Locked = sig ... end

module Coq_finfun : Coq_finfun_Locked