# Lesson VI
The drop shows its form; the brush sets it down.
## Try
```prolog
% ?- run([push(int(2)), push(int(3)), add], [], Stack).
% Stack = [int(5)].
% ?- infer([push(int(2)), push(int(3)), add], In, Out).
% In = [],
% Out = [int].
% ?- run([push(int(foo))], [], Stack).
% false.
```
## Learn
```prolog
% `push/1` validates a literal and puts it on the runtime stack
% unchanged.
apply(push(Value), Stack, [Value|Stack]) :-
lit(Value, _Type).
% `push/1` contributes the literal's type to the static stack.
infer1(push(Value), Stack, [Type|Stack]) :-
!,
lit(Value, Type).
% `lit/2` is the only way a literal enters runtime or inference.
lit(int(Int), int) :-
integer(Int).
```