diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-08 15:01:43 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-08 15:43:32 +0200 |
commit | 0ef1b22756cb35d80cfc47056e0f6f0401c151df (patch) | |
tree | e047749111ff7bf123d2ea9ef02f6f7b6c4b488b /engine | |
parent | bb63a9f2209108424bd3dadc1c479f9ddc0e1803 (diff) |
Add a bit of doc to EConstr.decompose_lam*
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index b0e834b2e..e9d3e782b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -182,9 +182,21 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint val decompose_app : Evd.evar_map -> t -> t * t list +(** Pops lambda abstractions until there are no more, skipping casts. *) val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t + +(** Pops lambda abstractions and letins until there are no more, skipping casts. *) val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t + +(** Pops [n] lambda abstractions, and pop letins only if needed to + expose enough lambdas, skipping casts. + + @raise UserError if the term doesn't have enough lambdas. *) val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t + +(** Pops [n] lambda abstractions and letins, skipping casts. + + @raise UserError if the term doesn't have enough lambdas/letins. *) val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t val compose_lam : (Name.t * t) list -> t -> t |