Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
tlringer authored Nov 16, 2017
1 parent 0fd26a2 commit f98eb72
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,7 @@ The core of PUMPKIN is a set of five core components. We expose four of those co
1. `Invert trm as id`: given `trm : ... -> T1 -> T2`, search for an inverse term `id : ... -> T2 -> T1`
2. `Specialize (fun args => f args) as id)`: apply `f` to `args`, reduce the result, and define this as `id`
3. `Abstract trm to typ as id`: abstract `trm` to a term `id : typ`
4. `Factor trm using prefix id`: given `trm : T1 -> T2 -> ... -> Tn`, search for factors `id_1: T1 -> T2`, ... , `id_n-1: Tn-1 -> Tn`
4. `Factor trm using prefix id`: given `trm : T1 -> Tn`, search for factors `id_1: T1 -> T2`, ... , `id_n-1: Tn-1 -> Tn`

There is also an experimental theorem patching command:

Expand Down

0 comments on commit f98eb72

Please sign in to comment.