-
Notifications
You must be signed in to change notification settings - Fork 10
Open
Description
Adding Foundation to an existing application fails with the following error message:
import Foundation.Vorspiel.Vorspiel failed, environment already contains 'Matrix.map.eq_1' from Mathlib.LinearAlgebra.Matrix.BaseChange
Environment: Linux Mint: 5.4.0-216-generic
'lakefile.tom' file:
name = "modal-logic"
version = "0.1.0"
defaultTargets = ["modal-logic"][[lean_lib]]
name = "ModalLogic"[[lean_exe]]
name = "modal-logic"
root = "Main"[[require]]
name = "Foundation"
scope = "FormalizedFormalLogic"
git = "https://github.com/FormalizedFormalLogic/Foundation"
rev = "master"
'lean-toolchain' file:
leanprover/lean4:v4.22.0-rc4
iehality
Metadata
Metadata
Assignees
Labels
No labels