search

tezos / tezoscoq

working with coq and tezos
28 stars 9 forks source link

stack_type should be list type #1

Open CoinFormalizer opened 7 years ago

CoinFormalizer commented 7 years ago

Right now stack type is defined as

with stack_type := | empty_stack : stack_type | cons_stack : type -> stack_type -> stack_type

but it should be something as close as possible to list type.