lean4-htt/tests/lean/366.lean.expected.out
Leonardo de Moura 99e8a98f06 feat: allow universes metavariables from any depth to be assigned when ignoreLevelDepth is true
We set `ignoreLevelDepth` to true during type class resolution.
2021-08-18 20:20:51 -07:00

13 lines
706 B
Text

[Meta.synthInstance] preprocess: Inhabited Nat ==> Inhabited Nat
[Meta.synthInstance]
[Meta.synthInstance] main goal Inhabited Nat
[Meta.synthInstance.newSubgoal] Inhabited Nat
[Meta.synthInstance.globalInstances] Inhabited Nat, [instInhabited, instInhabitedNat]
[Meta.synthInstance.generate] instance instInhabitedNat
[Meta.synthInstance.tryResolve]
[Meta.synthInstance.tryResolve] Inhabited Nat =?= Inhabited Nat
[Meta.synthInstance.tryResolve] success
[Meta.synthInstance.newAnswer] size: 0, Inhabited Nat
[Meta.synthInstance.newAnswer] val: instInhabitedNat
[Meta.synthInstance] FOUND result instInhabitedNat
[Meta.synthInstance] result instInhabitedNat