7 lines
155 B
Text
7 lines
155 B
Text
import algebra.bundled
|
|
variable G : Group
|
|
check (1 : G)
|
|
check (1 : Group.carrier G)
|
|
set_option pp.coercions true
|
|
check (1 : G)
|
|
check (1 : Group.carrier G)
|