Skip to content
Snippets Groups Projects
Commit 14a52d3f authored by gabrielhdt's avatar gabrielhdt
Browse files

Adding test for dependent types

parent c66e2824
No related branches found
No related tags found
No related merge requests found
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
require open personoj.encodings.deptype
require open personoj.encodings.prenex
symbol nat: θ {|set|}
symbol vect: ϕ (∀K (λ_, scheme_k (nat *> {|set|})))
assert vect: Set → η nat → Set
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment