Skip to content

Searching through notations #16

@sven--

Description

@sven--

While looking at cstep ((com * state) -> (com * state) -> Prop),
I wanted to revisit the definition of ().
However, (Print "
") only shows me the message below.

mult =
fix mult (n m : nat) {struct n} : nat :=
match n with
| 0 => 0
| S p => m + mult p m
end
: nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions