Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Unfoldable projection definitions: all
Cut: emp
For any goal ->
For nat -> simple apply 0 ; trivial (cost 1, pattern nat, id 0)
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Unfoldable projection definitions: all
Cut: emp
For any goal ->
For nat -> simple apply 0 ; trivial (cost 1, pattern nat, id 0)
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Unfoldable projection definitions: all
Cut: emp
For any goal ->
For nat -> simple apply 0 ; trivial (cost 1, pattern nat, id 0)
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
File "./output/HintLocality.v", line 61, characters 0-38:
The command has indeed failed with message:
This command does not support the global attribute in sections.
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat ->
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all except: id
Unfoldable projection definitions: all
Cut: _
For any goal ->
For S (modes !) ->
For nat -> simple apply 0 ; trivial (cost 1, pattern nat, id 0)
File "./output/HintLocality.v", line 92, characters 0-39:
Warning: This hint is not local but depends on a section variable. It will
disappear when the section is closed.
[non-local-section-hint,automation,default]
File "./output/HintLocality.v", line 94, characters 0-40:
Warning: This hint is not local but depends on a section variable. It will
disappear when the section is closed.
[non-local-section-hint,automation,default]
File "./output/HintLocality.v", line 98, characters 0-39:
Warning: This hint is not local but depends on a section variable. It will
disappear when the section is closed.
[non-local-section-hint,automation,default]
Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Unfoldable projection definitions: all
Cut: emp
For any goal ->
For refl (modes - !) ->
[ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
]
