src-coq/Queue.v · master · Li-yao Xia / hs-to-coq-tutorial · GitLab

Find file Blame History Permalink

Declare `models` as a `Definition` instead of `Inductive` · 17ec7ff3
Li-yao Xia authored Oct 04, 2020
```
Using projections instead of pattern-matching (simpler to explain)
```
17ec7ff3