simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix

Browse source
This commit is contained in:
Simon Cruanes 2023-03-06 23:42:37 -05:00
parent 42c6d2f770
commit 401365e1bb
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ciclib/term.ml
View file

@ -219,7 +219,7 @@ let db_replace_ e (env : t list) : term =
| E_const _ -> e
| E_bound_var v when v.bv_idx >= k && v.bv_idx < k + len_env ->
(* replace [v] with [env[v-k]], and shift it to account for the
[k] intermediate binders we traversed to get to [bv] *)
[k] intermediate binders we traversed to get to [v] *)
let u = List.nth env (v.bv_idx - k) in
db_shift_ u k
| _ ->
@ -244,8 +244,8 @@ let type_ : term = type_of_univ Level.one
let[@inline] bvar v : term = make_ (E_bound_var v)
let[@inline] bvar_i i : term = make_ (E_bound_var (Bvar.make i))
let[@inline] const c args : term = make_ (E_const (c, args))
let[@inline] app f a = make_ (E_app (f, a))
let[@inline] app_l f l = List.fold_left app f l
let[@inline] app f a : term = make_ (E_app (f, a))
let[@inline] app_l f l : term = List.fold_left app f l
let[@inline] lam b str ~var_ty bod : term = make_ (E_lam (b, str, var_ty, bod))
let[@inline] pi b str ~var_ty bod : term = make_ (E_pi (b, str, var_ty, bod))