max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: basic instances for ULift and PLift (#5112)

Browse source
This commit is contained in:
Kim Morrison 2024-08-21 21:37:13 +10:00 • committed by GitHub
parent a58da122b9
commit 0a8d1bf808
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data.lean
View file

@ -37,3 +37,5 @@ import Init.Data.Cast
import Init.Data.Sum
import Init.Data.BEq
import Init.Data.Subtype
import Init.Data.ULift
import Init.Data.PLift

12
src/Init/Data/PLift.lean Normal file
View file

@ -0,0 +1,12 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Core
deriving instance DecidableEq for PLift
instance [Subsingleton α] : Subsingleton (PLift α) where
allEq := fun ⟨a⟩ ⟨b⟩ => congrArg PLift.up (Subsingleton.elim a b)

12
src/Init/Data/ULift.lean Normal file
View file

@ -0,0 +1,12 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Core
deriving instance DecidableEq for ULift
instance [Subsingleton α] : Subsingleton (ULift α) where
allEq := fun ⟨a⟩ ⟨b⟩ => congrArg ULift.up (Subsingleton.elim a b)