8 lines
155 B
Text
8 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)
|