10 lines
418 B
Text
10 lines
418 B
Text
297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables
|
|
OfNat (Sort ?u) 0
|
|
297.lean:2:0-2:1: error: failed to synthesize instance
|
|
OfNat (Id PUnit) 0
|
|
297.lean:2:4-2:5: error: failed to synthesize instance
|
|
OfNat Prop 0
|
|
297.lean:1:10-1:11: error: failed to synthesize instance
|
|
OfNat (Type ?u) 0
|
|
297.lean:2:10-2:11: error: failed to synthesize instance
|
|
OfNat (Id PUnit) 0
|