Call to undefined function json_encode()

[treii28]

Fatal error: Uncaught Error: Call to undefined function json_encode() in /var/task/index.php:17

I added a php.ini to the root of my function as the (vague) instructions suggest.
I added extension_dir=/opt/lib/php/7.3/modules as ticket #2 suggests

Same error

php.ini contents:

extension_dir=/opt/lib/php/7.3/modules
extension=json.so