blob: 8c4808a755b27053607b5ee572d7aa742b115e39 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
open Names
let evil name name_f =
let open Univ in
let open Entries in
let open Constr in
let kind = Decls.(IsDefinition Definition) in
let u = Level.var 0 in
let tu = mkType (Universe.make u) in
let te = Declare.definition_entry
~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
in
let tc = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry te) in
let tc = mkConst tc in
let fe = Declare.definition_entry
~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
~types:(Term.mkArrowR tc tu)
(mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
in
let _ : Constant.t = Declare.declare_constant ~name:name_f ~kind (Declare.DefinitionEntry fe) in
()
|
