Skip to content
LogRel CI

use induction concl to specify DirectedAction #434

Sign in to view logs

use induction concl to specify DirectedAction

use induction concl to specify DirectedAction #434

Triggered via push October 3, 2023 08:49
@kyoDralliamkyoDralliam
pushed d581603
directions
Status Success
Total duration 7m 21s
Artifacts –

build.yml

on: push
build
7m 11s
build
Fit to window
Zoom out
Zoom in

Annotations

7 warnings
build
Argument B was previously inferred to be in scope type_scope but is
build
Argument B was previously inferred to be in scope type_scope but is
build
Argument B was previously inferred to be in the empty scope stack
build: theories/DirectedDeclarativeTyping.v#L10
The only parsing modifier has no effect in Reserved Notation.
build: theories/DirectedDeclarativeTyping.v#L11
The only parsing modifier has no effect in Reserved Notation.
build: theories/DirectedDeclarativeTyping.v#L12
The only parsing modifier has no effect in Reserved Notation.
build: theories/DirectedDeclarativeTyping.v#L13
The only parsing modifier has no effect in Reserved Notation.