1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Environ
open Evd
open EConstr
(** [telescope env sigma ctx] turns a context [x1:A1;...;xn:An] into a
right-associated nested sigma-type of the right sort. It returns:
- the nested sigma-type [T := {x1:A1 & ... {xn-1:An-1 & ... An} ... }]
- the canonical tuple [(existsT _ x1 ... (existsT _ xn-1 xn) ...)]
inhabiting the sigma-type in the given context
- an instantiation of the assumptions of [ctx] with values they
have in the context [x:T], that is
[x1:=projT1 x;...;xn-1:=projT1 ... (projT2 x);xn:=projT2 ... (projT2 x)];
note that let-ins in the original context are preserved
Depending on the sorts of types, it uses either [ex], [sig] or
[sigT], even if we always used [sigT] above as an example.
*)
type telescope = {
telescope_type : types;
telescope_value : constr;
}
val telescope : env -> evar_map -> rel_context -> evar_map * rel_context * telescope
(** [make_iterated_tuple env sigma ~default c] encapsulates [c] (of
inferred type [C]) and its free variables [x1,...,xn] into a
right-associated nested tuple in a [sigT]-type. It returns:
- the nested type [{x1:A1 & ... {xn:An & ... C} ... }]
- the tuple [(existsT _ x1 ... (existsT _ xn c) ...)]
- an alternative tuple [(existsT _ x1 ... (existsT _ xn default) ...)];
if [default] has not the right type, it fails.
*)
val make_iterated_tuple : env -> evar_map -> default:constr -> constr -> types -> evar_map * telescope * constr
(** [make_selector env sigma ~pos ~special ~default c] constructs a
case-split on [c] (assumed of inductive type), with the [pos]-th
branch returning [special], and all the other branch returning
[default]. *)
val make_selector : env -> evar_map -> pos:int -> special:constr -> default:constr -> constr -> types -> constr
|
