summaryrefslogtreecommitdiff
path: root/compiler/LlbcAst.ml
blob: f4d26e18fb4a1b3f24c00ad7811b212ef3252e94 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
open Types
open Values
include Charon.LlbcAst

type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
[@@deriving show]

type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
[@@deriving show]

(** A function signature, after instantiation *)
type inst_fun_sig = {
  regions_hierarchy : abs_region_groups;
  inputs : rty list;
  output : rty;
}
[@@deriving show]