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

chore: mark MutQuot.val as [neverExtract]

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-07 11:43:14 -08:00
parent 354439dd43
commit d9ca2751c2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/MutQuot.lean
View file

@ -12,7 +12,7 @@ structure MutQuot {α : Type u} (r : α → α → Prop) :=
mkAux :: (val : Quot r)
attribute [extern "lean_mutquot_mk"] MutQuot.mkAux
attribute [extern "lean_mutquot_get"] MutQuot.val
attribute [extern "lean_mutquot_get", neverExtract] MutQuot.val
@[extern "lean_mutquot_mk"]
def MutQuot.mk {α : Type u} (r : α → α → Prop) (a : α) : MutQuot r :=