Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
351e5533
Commit
351e5533
authored
Nov 24, 2021
by
Michael Sammler
Browse files
add Strategy expand
parent
74189201
Pipeline
#57785
passed with stage
in 11 minutes and 38 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/lithium/interpreter.v
View file @
351e5533
...
...
@@ -7,12 +7,15 @@ Notation "'HIDDEN'" := (Envs _ _ _) (only printing).
Definition
LET_ID
{
A
}
(
x
:
A
)
:
A
:
=
x
.
Arguments
LET_ID
:
simpl
never
.
Notation
"'HIDDEN'"
:
=
(
LET_ID
_
)
(
only
printing
).
Strategy
expand
[
LET_ID
].
Definition
EVAR_ID
{
A
}
(
x
:
A
)
:
A
:
=
x
.
Arguments
EVAR_ID
:
simpl
never
.
Strategy
expand
[
EVAR_ID
].
Definition
SHELVED_SIDECOND
(
P
:
Prop
)
:
Prop
:
=
P
.
Arguments
SHELVED_SIDECOND
:
simpl
never
.
Strategy
expand
[
SHELVED_SIDECOND
].
(** * Lemmas used by tactics *)
Section
coq_tactics
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment