feat(kernel): add mk_hott_environment function for creating HoTT compatible environments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
4d1fecb21d
commit
45d473d44e
4 changed files with 37 additions and 0 deletions
|
@ -217,6 +217,8 @@ add_subdirectory(kernel/inductive)
|
|||
set(LEAN_LIBS ${LEAN_LIBS} inductive)
|
||||
add_subdirectory(kernel/standard)
|
||||
set(LEAN_LIBS ${LEAN_LIBS} standard_kernel)
|
||||
add_subdirectory(kernel/hott)
|
||||
set(LEAN_LIBS ${LEAN_LIBS} hott_kernel)
|
||||
add_subdirectory(library)
|
||||
set(LEAN_LIBS ${LEAN_LIBS} library)
|
||||
# add_subdirectory(library/rewriter)
|
||||
|
|
2
src/kernel/hott/CMakeLists.txt
Normal file
2
src/kernel/hott/CMakeLists.txt
Normal file
|
@ -0,0 +1,2 @@
|
|||
add_library(hott_kernel hott.cpp)
|
||||
target_link_libraries(hott_kernel ${LEAN_LIBS})
|
22
src/kernel/hott/hott.cpp
Normal file
22
src/kernel/hott/hott.cpp
Normal file
|
@ -0,0 +1,22 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "kernel/inductive/inductive.h"
|
||||
|
||||
namespace lean {
|
||||
using inductive::inductive_normalizer_extension;
|
||||
|
||||
/** \brief Create a HoTT (Homotopy Type Theory) compatible environment */
|
||||
environment mk_hott_environment(unsigned trust_lvl) {
|
||||
return environment(trust_lvl,
|
||||
false /* Type.{0} is proof relevant */,
|
||||
true /* Eta */,
|
||||
false /* Type.{0} is predicative */,
|
||||
list<name>(name("Id")) /* Exact equality types are proof irrelevant */,
|
||||
/* builtin support for inductive datatypes */
|
||||
std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()));
|
||||
}
|
||||
}
|
11
src/kernel/hott/hott.h
Normal file
11
src/kernel/hott/hott.h
Normal file
|
@ -0,0 +1,11 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/environment.h"
|
||||
namespace lean {
|
||||
environment mk_hott_environment(unsigned trust_lvl = 0);
|
||||
}
|
Loading…
Reference in a new issue