You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
|
|
-Q theories/lib semantics.lib
|
|
|
|
|
-Q theories/type_systems semantics.ts
|
|
|
|
|
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
|
|
|
|
|
-arg -w -arg -notation-overridden
|
|
|
|
|
# Cannot use non-canonical projections as it causes massive unification failures
|
|
|
|
|
# (https://github.com/coq/coq/issues/6294).
|
|
|
|
|
-arg -w -arg -redundant-canonical-projection
|
|
|
|
|
# we use Restart for demoing purposes, sometimes
|
|
|
|
|
-arg -w -arg -undo-batch-mode
|
|
|
|
|
|
|
|
|
|
# library stuff
|
|
|
|
|
theories/lib/maps.v
|
|
|
|
|
theories/lib/sets.v
|
|
|
|
|
|
|
|
|
|
# STLC
|
|
|
|
|
theories/type_systems/stlc/lang.v
|
|
|
|
|
theories/type_systems/stlc/notation.v
|
|
|
|
|
|
|
|
|
|
# By removing the # below, you can add the exercise sheets to make
|
|
|
|
|
#theories/type_systems/warmup/warmup.v
|
|
|
|
|
#theories/type_systems/warmup/warmup_sol.v
|
|
|
|
|
#theories/type_systems/stlc/exercises01.v
|
|
|
|
|
#theories/type_systems/stlc/exercises01_sol.v
|
